Metamath Proof Explorer

Theorem fodomr

Description: There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006)

Ref Expression
Assertion fodomr 
|- ( ( (/) ~< B /\ B ~<_ A ) -> E. f f : A -onto-> B )

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex2i 
 |-  ( B ~<_ A -> A e. _V )
3 2 adantl 
 |-  ( ( (/) ~< B /\ B ~<_ A ) -> A e. _V )
4 1 brrelex1i 
 |-  ( B ~<_ A -> B e. _V )
5 0sdomg 
 |-  ( B e. _V -> ( (/) ~< B <-> B =/= (/) ) )
6 n0 
 |-  ( B =/= (/) <-> E. z z e. B )
7 5 6 bitrdi 
 |-  ( B e. _V -> ( (/) ~< B <-> E. z z e. B ) )
8 4 7 syl 
 |-  ( B ~<_ A -> ( (/) ~< B <-> E. z z e. B ) )
9 8 biimpac 
 |-  ( ( (/) ~< B /\ B ~<_ A ) -> E. z z e. B )
10 brdomi 
 |-  ( B ~<_ A -> E. g g : B -1-1-> A )
11 10 adantl 
 |-  ( ( (/) ~< B /\ B ~<_ A ) -> E. g g : B -1-1-> A )
12 difexg 
 |-  ( A e. _V -> ( A \ ran g ) e. _V )
13 vsnex 
 |-  { z } e. _V
14 xpexg 
 |-  ( ( ( A \ ran g ) e. _V /\ { z } e. _V ) -> ( ( A \ ran g ) X. { z } ) e. _V )
15 12 13 14 sylancl 
 |-  ( A e. _V -> ( ( A \ ran g ) X. { z } ) e. _V )
16 vex 
 |-  g e. _V
17 16 cnvex 
 |-  `' g e. _V
18 15 17 jctil 
 |-  ( A e. _V -> ( `' g e. _V /\ ( ( A \ ran g ) X. { z } ) e. _V ) )
19 unexb 
 |-  ( ( `' g e. _V /\ ( ( A \ ran g ) X. { z } ) e. _V ) <-> ( `' g u. ( ( A \ ran g ) X. { z } ) ) e. _V )
20 18 19 sylib 
 |-  ( A e. _V -> ( `' g u. ( ( A \ ran g ) X. { z } ) ) e. _V )
21 df-f1 
 |-  ( g : B -1-1-> A <-> ( g : B --> A /\ Fun `' g ) )
22 21 simprbi 
 |-  ( g : B -1-1-> A -> Fun `' g )
23 vex 
 |-  z e. _V
24 23 fconst 
 |-  ( ( A \ ran g ) X. { z } ) : ( A \ ran g ) --> { z }
25 ffun 
 |-  ( ( ( A \ ran g ) X. { z } ) : ( A \ ran g ) --> { z } -> Fun ( ( A \ ran g ) X. { z } ) )
26 24 25 ax-mp 
 |-  Fun ( ( A \ ran g ) X. { z } )
27 22 26 jctir 
 |-  ( g : B -1-1-> A -> ( Fun `' g /\ Fun ( ( A \ ran g ) X. { z } ) ) )
28 df-rn 
 |-  ran g = dom `' g
29 28 eqcomi 
 |-  dom `' g = ran g
30 23 snnz 
 |-  { z } =/= (/)
31 dmxp 
 |-  ( { z } =/= (/) -> dom ( ( A \ ran g ) X. { z } ) = ( A \ ran g ) )
32 30 31 ax-mp 
 |-  dom ( ( A \ ran g ) X. { z } ) = ( A \ ran g )
33 29 32 ineq12i 
 |-  ( dom `' g i^i dom ( ( A \ ran g ) X. { z } ) ) = ( ran g i^i ( A \ ran g ) )
34 disjdif 
 |-  ( ran g i^i ( A \ ran g ) ) = (/)
35 33 34 eqtri 
 |-  ( dom `' g i^i dom ( ( A \ ran g ) X. { z } ) ) = (/)
36 funun 
 |-  ( ( ( 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 } ) ) )
37 27 35 36 sylancl 
 |-  ( g : B -1-1-> A -> Fun ( `' g u. ( ( A \ ran g ) X. { z } ) ) )
38 37 adantl 
 |-  ( ( z e. B /\ g : B -1-1-> A ) -> Fun ( `' g u. ( ( A \ ran g ) X. { z } ) ) )
39 dmun 
 |-  dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = ( dom `' g u. dom ( ( A \ ran g ) X. { z } ) )
40 28 uneq1i 
 |-  ( ran g u. dom ( ( A \ ran g ) X. { z } ) ) = ( dom `' g u. dom ( ( A \ ran g ) X. { z } ) )
41 32 uneq2i 
 |-  ( ran g u. dom ( ( A \ ran g ) X. { z } ) ) = ( ran g u. ( A \ ran g ) )
42 39 40 41 3eqtr2i 
 |-  dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = ( ran g u. ( A \ ran g ) )
43 f1f 
 |-  ( g : B -1-1-> A -> g : B --> A )
44 43 frnd 
 |-  ( g : B -1-1-> A -> ran g C_ A )
45 undif 
 |-  ( ran g C_ A <-> ( ran g u. ( A \ ran g ) ) = A )
46 44 45 sylib 
 |-  ( g : B -1-1-> A -> ( ran g u. ( A \ ran g ) ) = A )
47 42 46 eqtrid 
 |-  ( g : B -1-1-> A -> dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = A )
48 47 adantl 
 |-  ( ( z e. B /\ g : B -1-1-> A ) -> dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = A )
49 df-fn 
 |-  ( ( `' 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 ) )
50 38 48 49 sylanbrc 
 |-  ( ( z e. B /\ g : B -1-1-> A ) -> ( `' g u. ( ( A \ ran g ) X. { z } ) ) Fn A )
51 rnun 
 |-  ran ( `' g u. ( ( A \ ran g ) X. { z } ) ) = ( ran `' g u. ran ( ( A \ ran g ) X. { z } ) )
52 dfdm4 
 |-  dom g = ran `' g
53 f1dm 
 |-  ( g : B -1-1-> A -> dom g = B )
54 52 53 eqtr3id 
 |-  ( g : B -1-1-> A -> ran `' g = B )
55 54 uneq1d 
 |-  ( g : B -1-1-> A -> ( ran `' g u. ran ( ( A \ ran g ) X. { z } ) ) = ( B u. ran ( ( A \ ran g ) X. { z } ) ) )
56 xpeq1 
 |-  ( ( A \ ran g ) = (/) -> ( ( A \ ran g ) X. { z } ) = ( (/) X. { z } ) )
57 0xp 
 |-  ( (/) X. { z } ) = (/)
58 56 57 eqtrdi 
 |-  ( ( A \ ran g ) = (/) -> ( ( A \ ran g ) X. { z } ) = (/) )
59 58 rneqd 
 |-  ( ( A \ ran g ) = (/) -> ran ( ( A \ ran g ) X. { z } ) = ran (/) )
60 rn0 
 |-  ran (/) = (/)
61 59 60 eqtrdi 
 |-  ( ( A \ ran g ) = (/) -> ran ( ( A \ ran g ) X. { z } ) = (/) )
62 0ss 
 |-  (/) C_ B
63 61 62 eqsstrdi 
 |-  ( ( A \ ran g ) = (/) -> ran ( ( A \ ran g ) X. { z } ) C_ B )
64 63 a1d 
 |-  ( ( A \ ran g ) = (/) -> ( z e. B -> ran ( ( A \ ran g ) X. { z } ) C_ B ) )
65 rnxp 
 |-  ( ( A \ ran g ) =/= (/) -> ran ( ( A \ ran g ) X. { z } ) = { z } )
66 65 adantr 
 |-  ( ( ( A \ ran g ) =/= (/) /\ z e. B ) -> ran ( ( A \ ran g ) X. { z } ) = { z } )
67 snssi 
 |-  ( z e. B -> { z } C_ B )
68 67 adantl 
 |-  ( ( ( A \ ran g ) =/= (/) /\ z e. B ) -> { z } C_ B )
69 66 68 eqsstrd 
 |-  ( ( ( A \ ran g ) =/= (/) /\ z e. B ) -> ran ( ( A \ ran g ) X. { z } ) C_ B )
70 69 ex 
 |-  ( ( A \ ran g ) =/= (/) -> ( z e. B -> ran ( ( A \ ran g ) X. { z } ) C_ B ) )
71 64 70 pm2.61ine 
 |-  ( z e. B -> ran ( ( A \ ran g ) X. { z } ) C_ B )
72 ssequn2 
 |-  ( ran ( ( A \ ran g ) X. { z } ) C_ B <-> ( B u. ran ( ( A \ ran g ) X. { z } ) ) = B )
73 71 72 sylib 
 |-  ( z e. B -> ( B u. ran ( ( A \ ran g ) X. { z } ) ) = B )
74 55 73 sylan9eqr 
 |-  ( ( z e. B /\ g : B -1-1-> A ) -> ( ran `' g u. ran ( ( A \ ran g ) X. { z } ) ) = B )
75 51 74 eqtrid 
 |-  ( ( z e. B /\ g : B -1-1-> A ) -> ran ( `' g u. ( ( A \ ran g ) X. { z } ) ) = B )
76 df-fo 
 |-  ( ( `' 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 ) )
77 50 75 76 sylanbrc 
 |-  ( ( z e. B /\ g : B -1-1-> A ) -> ( `' g u. ( ( A \ ran g ) X. { z } ) ) : A -onto-> B )
78 foeq1 
 |-  ( f = ( `' g u. ( ( A \ ran g ) X. { z } ) ) -> ( f : A -onto-> B <-> ( `' g u. ( ( A \ ran g ) X. { z } ) ) : A -onto-> B ) )
79 78 spcegv 
 |-  ( ( `' 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 ) )
80 20 77 79 syl2im 
 |-  ( A e. _V -> ( ( z e. B /\ g : B -1-1-> A ) -> E. f f : A -onto-> B ) )
81 80 expdimp 
 |-  ( ( A e. _V /\ z e. B ) -> ( g : B -1-1-> A -> E. f f : A -onto-> B ) )
82 81 exlimdv 
 |-  ( ( A e. _V /\ z e. B ) -> ( E. g g : B -1-1-> A -> E. f f : A -onto-> B ) )
83 82 ex 
 |-  ( A e. _V -> ( z e. B -> ( E. g g : B -1-1-> A -> E. f f : A -onto-> B ) ) )
84 83 exlimdv 
 |-  ( A e. _V -> ( E. z z e. B -> ( E. g g : B -1-1-> A -> E. f f : A -onto-> B ) ) )
85 3 9 11 84 syl3c 
 |-  ( ( (/) ~< B /\ B ~<_ A ) -> E. f f : A -onto-> B )