This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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→ 𝐵 )