Metamath Proof Explorer

Theorem fodomfir

Description: There exists a mapping from a finite set onto any nonempty set that it dominates, proved without using the Axiom of Power Sets (unlike fodomr ). (Contributed by BTernaryTau, 23-Jun-2025)

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

Proof

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