MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fodomr Structured version   Visualization version   Unicode version

Theorem fodomr 7741
Description: There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.)
Assertion
Ref Expression
fodomr  |-  ( (
(/)  ~<  B  /\  B  ~<_  A )  ->  E. f 
f : A -onto-> B
)
Distinct variable groups:    A, f    B, f

Proof of Theorem fodomr
Dummy variables  g 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 7593 . . . 4  |-  Rel  ~<_
21brrelex2i 4881 . . 3  |-  ( B  ~<_  A  ->  A  e.  _V )
32adantl 473 . 2  |-  ( (
(/)  ~<  B  /\  B  ~<_  A )  ->  A  e.  _V )
41brrelexi 4880 . . . 4  |-  ( B  ~<_  A  ->  B  e.  _V )
5 0sdomg 7719 . . . . 5  |-  ( B  e.  _V  ->  ( (/) 
~<  B  <->  B  =/=  (/) ) )
6 n0 3732 . . . . 5  |-  ( B  =/=  (/)  <->  E. z  z  e.  B )
75, 6syl6bb 269 . . . 4  |-  ( B  e.  _V  ->  ( (/) 
~<  B  <->  E. z  z  e.  B ) )
84, 7syl 17 . . 3  |-  ( B  ~<_  A  ->  ( (/)  ~<  B  <->  E. z 
z  e.  B ) )
98biimpac 494 . 2  |-  ( (
(/)  ~<  B  /\  B  ~<_  A )  ->  E. z 
z  e.  B )
10 brdomi 7598 . . 3  |-  ( B  ~<_  A  ->  E. g 
g : B -1-1-> A
)
1110adantl 473 . 2  |-  ( (
(/)  ~<  B  /\  B  ~<_  A )  ->  E. g 
g : B -1-1-> A
)
12 difexg 4545 . . . . . . . . . 10  |-  ( A  e.  _V  ->  ( A  \  ran  g )  e.  _V )
13 snex 4641 . . . . . . . . . 10  |-  { z }  e.  _V
14 xpexg 6612 . . . . . . . . . 10  |-  ( ( ( A  \  ran  g )  e.  _V  /\ 
{ z }  e.  _V )  ->  ( ( A  \  ran  g
)  X.  { z } )  e.  _V )
1512, 13, 14sylancl 675 . . . . . . . . 9  |-  ( A  e.  _V  ->  (
( A  \  ran  g )  X.  {
z } )  e. 
_V )
16 vex 3034 . . . . . . . . . 10  |-  g  e. 
_V
1716cnvex 6759 . . . . . . . . 9  |-  `' g  e.  _V
1815, 17jctil 546 . . . . . . . 8  |-  ( A  e.  _V  ->  ( `' g  e.  _V  /\  ( ( A  \  ran  g )  X.  {
z } )  e. 
_V ) )
19 unexb 6610 . . . . . . . 8  |-  ( ( `' g  e.  _V  /\  ( ( A  \  ran  g )  X.  {
z } )  e. 
_V )  <->  ( `' g  u.  ( ( A  \  ran  g )  X.  { z } ) )  e.  _V )
2018, 19sylib 201 . . . . . . 7  |-  ( A  e.  _V  ->  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  e.  _V )
21 df-f1 5594 . . . . . . . . . . . . 13  |-  ( g : B -1-1-> A  <->  ( g : B --> A  /\  Fun  `' g ) )
2221simprbi 471 . . . . . . . . . . . 12  |-  ( g : B -1-1-> A  ->  Fun  `' g )
23 vex 3034 . . . . . . . . . . . . . 14  |-  z  e. 
_V
2423fconst 5782 . . . . . . . . . . . . 13  |-  ( ( A  \  ran  g
)  X.  { z } ) : ( A  \  ran  g
) --> { z }
25 ffun 5742 . . . . . . . . . . . . 13  |-  ( ( ( A  \  ran  g )  X.  {
z } ) : ( A  \  ran  g ) --> { z }  ->  Fun  ( ( A  \  ran  g
)  X.  { z } ) )
2624, 25ax-mp 5 . . . . . . . . . . . 12  |-  Fun  (
( A  \  ran  g )  X.  {
z } )
2722, 26jctir 547 . . . . . . . . . . 11  |-  ( g : B -1-1-> A  -> 
( Fun  `' g  /\  Fun  ( ( A 
\  ran  g )  X.  { z } ) ) )
28 df-rn 4850 . . . . . . . . . . . . . 14  |-  ran  g  =  dom  `' g
2928eqcomi 2480 . . . . . . . . . . . . 13  |-  dom  `' g  =  ran  g
3023snnz 4081 . . . . . . . . . . . . . 14  |-  { z }  =/=  (/)
31 dmxp 5059 . . . . . . . . . . . . . 14  |-  ( { z }  =/=  (/)  ->  dom  ( ( A  \  ran  g )  X.  {
z } )  =  ( A  \  ran  g ) )
3230, 31ax-mp 5 . . . . . . . . . . . . 13  |-  dom  (
( A  \  ran  g )  X.  {
z } )  =  ( A  \  ran  g )
3329, 32ineq12i 3623 . . . . . . . . . . . 12  |-  ( dom  `' g  i^i  dom  (
( A  \  ran  g )  X.  {
z } ) )  =  ( ran  g  i^i  ( A  \  ran  g ) )
34 disjdif 3830 . . . . . . . . . . . 12  |-  ( ran  g  i^i  ( A 
\  ran  g )
)  =  (/)
3533, 34eqtri 2493 . . . . . . . . . . 11  |-  ( dom  `' g  i^i  dom  (
( A  \  ran  g )  X.  {
z } ) )  =  (/)
36 funun 5631 . . . . . . . . . . 11  |-  ( ( ( Fun  `' g  /\  Fun  ( ( A  \  ran  g
)  X.  { z } ) )  /\  ( dom  `' g  i^i 
dom  ( ( A 
\  ran  g )  X.  { z } ) )  =  (/) )  ->  Fun  ( `' g  u.  ( ( A  \  ran  g )  X.  {
z } ) ) )
3727, 35, 36sylancl 675 . . . . . . . . . 10  |-  ( g : B -1-1-> A  ->  Fun  ( `' g  u.  ( ( A  \  ran  g )  X.  {
z } ) ) )
3837adantl 473 . . . . . . . . 9  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  Fun  ( `' g  u.  ( ( A  \  ran  g )  X.  { z } ) ) )
39 dmun 5047 . . . . . . . . . . . 12  |-  dom  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  =  ( dom  `' g  u.  dom  ( ( A  \  ran  g
)  X.  { z } ) )
4028uneq1i 3575 . . . . . . . . . . . 12  |-  ( ran  g  u.  dom  (
( A  \  ran  g )  X.  {
z } ) )  =  ( dom  `' g  u.  dom  ( ( A  \  ran  g
)  X.  { z } ) )
4132uneq2i 3576 . . . . . . . . . . . 12  |-  ( ran  g  u.  dom  (
( A  \  ran  g )  X.  {
z } ) )  =  ( ran  g  u.  ( A  \  ran  g ) )
4239, 40, 413eqtr2i 2499 . . . . . . . . . . 11  |-  dom  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  =  ( ran  g  u.  ( A  \  ran  g ) )
43 f1f 5792 . . . . . . . . . . . . 13  |-  ( g : B -1-1-> A  -> 
g : B --> A )
44 frn 5747 . . . . . . . . . . . . 13  |-  ( g : B --> A  ->  ran  g  C_  A )
4543, 44syl 17 . . . . . . . . . . . 12  |-  ( g : B -1-1-> A  ->  ran  g  C_  A )
46 undif 3839 . . . . . . . . . . . 12  |-  ( ran  g  C_  A  <->  ( ran  g  u.  ( A  \  ran  g ) )  =  A )
4745, 46sylib 201 . . . . . . . . . . 11  |-  ( g : B -1-1-> A  -> 
( ran  g  u.  ( A  \  ran  g
) )  =  A )
4842, 47syl5eq 2517 . . . . . . . . . 10  |-  ( g : B -1-1-> A  ->  dom  ( `' g  u.  ( ( A  \  ran  g )  X.  {
z } ) )  =  A )
4948adantl 473 . . . . . . . . 9  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  dom  ( `' g  u.  ( ( A  \  ran  g )  X.  { z } ) )  =  A )
50 df-fn 5592 . . . . . . . . 9  |-  ( ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  Fn  A  <->  ( Fun  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  /\  dom  ( `' g  u.  ( ( A  \  ran  g
)  X.  { z } ) )  =  A ) )
5138, 49, 50sylanbrc 677 . . . . . . . 8  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  ( `' g  u.  ( ( A 
\  ran  g )  X.  { z } ) )  Fn  A )
52 rnun 5250 . . . . . . . . 9  |-  ran  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  =  ( ran  `' g  u.  ran  ( ( A  \  ran  g
)  X.  { z } ) )
53 dfdm4 5032 . . . . . . . . . . . 12  |-  dom  g  =  ran  `' g
54 f1dm 5796 . . . . . . . . . . . 12  |-  ( g : B -1-1-> A  ->  dom  g  =  B
)
5553, 54syl5eqr 2519 . . . . . . . . . . 11  |-  ( g : B -1-1-> A  ->  ran  `' g  =  B
)
5655uneq1d 3578 . . . . . . . . . 10  |-  ( g : B -1-1-> A  -> 
( ran  `' g  u.  ran  ( ( A 
\  ran  g )  X.  { z } ) )  =  ( B  u.  ran  ( ( A  \  ran  g
)  X.  { z } ) ) )
57 xpeq1 4853 . . . . . . . . . . . . . . . . 17  |-  ( ( A  \  ran  g
)  =  (/)  ->  (
( A  \  ran  g )  X.  {
z } )  =  ( (/)  X.  { z } ) )
58 0xp 4920 . . . . . . . . . . . . . . . . 17  |-  ( (/)  X. 
{ z } )  =  (/)
5957, 58syl6eq 2521 . . . . . . . . . . . . . . . 16  |-  ( ( A  \  ran  g
)  =  (/)  ->  (
( A  \  ran  g )  X.  {
z } )  =  (/) )
6059rneqd 5068 . . . . . . . . . . . . . . 15  |-  ( ( A  \  ran  g
)  =  (/)  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  =  ran  (/) )
61 rn0 5092 . . . . . . . . . . . . . . 15  |-  ran  (/)  =  (/)
6260, 61syl6eq 2521 . . . . . . . . . . . . . 14  |-  ( ( A  \  ran  g
)  =  (/)  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  =  (/) )
63 0ss 3766 . . . . . . . . . . . . . 14  |-  (/)  C_  B
6462, 63syl6eqss 3468 . . . . . . . . . . . . 13  |-  ( ( A  \  ran  g
)  =  (/)  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B )
6564a1d 25 . . . . . . . . . . . 12  |-  ( ( A  \  ran  g
)  =  (/)  ->  (
z  e.  B  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B ) )
66 rnxp 5273 . . . . . . . . . . . . . . 15  |-  ( ( A  \  ran  g
)  =/=  (/)  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  =  { z } )
6766adantr 472 . . . . . . . . . . . . . 14  |-  ( ( ( A  \  ran  g )  =/=  (/)  /\  z  e.  B )  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  =  { z } )
68 snssi 4107 . . . . . . . . . . . . . . 15  |-  ( z  e.  B  ->  { z }  C_  B )
6968adantl 473 . . . . . . . . . . . . . 14  |-  ( ( ( A  \  ran  g )  =/=  (/)  /\  z  e.  B )  ->  { z }  C_  B )
7067, 69eqsstrd 3452 . . . . . . . . . . . . 13  |-  ( ( ( A  \  ran  g )  =/=  (/)  /\  z  e.  B )  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B )
7170ex 441 . . . . . . . . . . . 12  |-  ( ( A  \  ran  g
)  =/=  (/)  ->  (
z  e.  B  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B ) )
7265, 71pm2.61ine 2726 . . . . . . . . . . 11  |-  ( z  e.  B  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B )
73 ssequn2 3598 . . . . . . . . . . 11  |-  ( ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B 
<->  ( B  u.  ran  ( ( A  \  ran  g )  X.  {
z } ) )  =  B )
7472, 73sylib 201 . . . . . . . . . 10  |-  ( z  e.  B  ->  ( B  u.  ran  ( ( A  \  ran  g
)  X.  { z } ) )  =  B )
7556, 74sylan9eqr 2527 . . . . . . . . 9  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  ( ran  `' g  u.  ran  ( ( A  \  ran  g
)  X.  { z } ) )  =  B )
7652, 75syl5eq 2517 . . . . . . . 8  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  ran  ( `' g  u.  ( ( A  \  ran  g )  X.  { z } ) )  =  B )
77 df-fo 5595 . . . . . . . 8  |-  ( ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) ) : A -onto-> B  <->  ( ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  Fn  A  /\  ran  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  =  B ) )
7851, 76, 77sylanbrc 677 . . . . . . 7  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  ( `' g  u.  ( ( A 
\  ran  g )  X.  { z } ) ) : A -onto-> B
)
79 foeq1 5802 . . . . . . . 8  |-  ( f  =  ( `' g  u.  ( ( A 
\  ran  g )  X.  { z } ) )  ->  ( f : A -onto-> B  <->  ( `' g  u.  ( ( A 
\  ran  g )  X.  { z } ) ) : A -onto-> B
) )
8079spcegv 3121 . . . . . . 7  |-  ( ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  e.  _V  ->  (
( `' g  u.  ( ( A  \  ran  g )  X.  {
z } ) ) : A -onto-> B  ->  E. f  f : A -onto-> B ) )
8120, 78, 80syl2im 38 . . . . . 6  |-  ( A  e.  _V  ->  (
( z  e.  B  /\  g : B -1-1-> A
)  ->  E. f 
f : A -onto-> B
) )
8281expdimp 444 . . . . 5  |-  ( ( A  e.  _V  /\  z  e.  B )  ->  ( g : B -1-1-> A  ->  E. f  f : A -onto-> B ) )
8382exlimdv 1787 . . . 4  |-  ( ( A  e.  _V  /\  z  e.  B )  ->  ( E. g  g : B -1-1-> A  ->  E. f  f : A -onto-> B ) )
8483ex 441 . . 3  |-  ( A  e.  _V  ->  (
z  e.  B  -> 
( E. g  g : B -1-1-> A  ->  E. f  f : A -onto-> B ) ) )
8584exlimdv 1787 . 2  |-  ( A  e.  _V  ->  ( E. z  z  e.  B  ->  ( E. g 
g : B -1-1-> A  ->  E. f  f : A -onto-> B ) ) )
863, 9, 11, 85syl3c 62 1  |-  ( (
(/)  ~<  B  /\  B  ~<_  A )  ->  E. f 
f : A -onto-> B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    = wceq 1452   E.wex 1671    e. wcel 1904    =/= wne 2641   _Vcvv 3031    \ cdif 3387    u. cun 3388    i^i cin 3389    C_ wss 3390   (/)c0 3722   {csn 3959   class class class wbr 4395    X. cxp 4837   `'ccnv 4838   dom cdm 4839   ran crn 4840   Fun wfun 5583    Fn wfn 5584   -->wf 5585   -1-1->wf1 5586   -onto->wfo 5587    ~<_ cdom 7585    ~< csdm 7586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590
This theorem is referenced by:  pwdom  7742  fodomfib  7869  domwdom  8107  iunfictbso  8563  fodomb  8972  brdom3  8974  konigthlem  9011  1stcfb  20537  ovoliunnul  22538  sigapildsys  29058  carsgclctunlem3  29225  ovoliunnfl  32046  voliunnfl  32048  volsupnfl  32049  nnfoctb  37443  caragenunicl  38464
  Copyright terms: Public domain W3C validator