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 ( ( 𝐴 ∈ Fin ∧ ∅ ≺ 𝐵𝐵𝐴 ) → ∃ 𝑓 𝑓 : 𝐴onto𝐵 )

Proof

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