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 )