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

Proof

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