Metamath Proof Explorer

Theorem enfixsn

Description: Given two equipollent sets, a bijection can always be chosen which fixes a single point. (Contributed by Stefan O'Rear, 9-Jul-2015)

Ref Expression
Assertion enfixsn ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) → 𝑋 ≈ 𝑌 )
2 bren ⊢ ( 𝑋 ≈ 𝑌 ↔ ∃ 𝑔 𝑔 : 𝑋 –1-1-onto→ 𝑌 )
3 1 2 sylib ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) → ∃ 𝑔 𝑔 : 𝑋 –1-1-onto→ 𝑌 )
4 relen ⊢ Rel ≈
5 4 brrelex2i ⊢ ( 𝑋 ≈ 𝑌 → 𝑌 ∈ V )
6 5 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) → 𝑌 ∈ V )
7 6 adantr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → 𝑌 ∈ V )
8 f1of ⊢ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 → 𝑔 : 𝑋 ⟶ 𝑌 )
9 8 adantl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → 𝑔 : 𝑋 ⟶ 𝑌 )
10 simpl1 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → 𝐴 ∈ 𝑋 )
11 9 10 ffvelrnd ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑔 ‘ 𝐴 ) ∈ 𝑌 )
12 simpl2 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → 𝐵 ∈ 𝑌 )
13 difsnen ⊢ ( ( 𝑌 ∈ V ∧ ( 𝑔 ‘ 𝐴 ) ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) → ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ≈ ( 𝑌 ∖ { 𝐵 } ) )
14 7 11 12 13 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ≈ ( 𝑌 ∖ { 𝐵 } ) )
15 bren ⊢ ( ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ≈ ( 𝑌 ∖ { 𝐵 } ) ↔ ∃ ℎ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) )
16 14 15 sylib ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ∃ ℎ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) )
17 fvex ⊢ ( 𝑔 ‘ 𝐴 ) ∈ V
18 17 a1i ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( 𝑔 ‘ 𝐴 ) ∈ V )
19 simpl2 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → 𝐵 ∈ 𝑌 )
20 f1osng ⊢ ( ( ( 𝑔 ‘ 𝐴 ) ∈ V ∧ 𝐵 ∈ 𝑌 ) → { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } : { ( 𝑔 ‘ 𝐴 ) } –1-1-onto→ { 𝐵 } )
21 18 19 20 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } : { ( 𝑔 ‘ 𝐴 ) } –1-1-onto→ { 𝐵 } )
22 simprr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) )
23 disjdif ⊢ ( { ( 𝑔 ‘ 𝐴 ) } ∩ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = ∅
24 23 a1i ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { ( 𝑔 ‘ 𝐴 ) } ∩ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = ∅ )
25 disjdif ⊢ ( { 𝐵 } ∩ ( 𝑌 ∖ { 𝐵 } ) ) = ∅
26 25 a1i ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { 𝐵 } ∩ ( 𝑌 ∖ { 𝐵 } ) ) = ∅ )
27 f1oun ⊢ ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } : { ( 𝑔 ‘ 𝐴 ) } –1-1-onto→ { 𝐵 } ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ∧ ( ( { ( 𝑔 ‘ 𝐴 ) } ∩ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = ∅ ∧ ( { 𝐵 } ∩ ( 𝑌 ∖ { 𝐵 } ) ) = ∅ ) ) → ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) : ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) –1-1-onto→ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) )
28 21 22 24 26 27 syl22anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) : ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) –1-1-onto→ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) )
29 8 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → 𝑔 : 𝑋 ⟶ 𝑌 )
30 simpl1 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → 𝐴 ∈ 𝑋 )
31 29 30 ffvelrnd ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( 𝑔 ‘ 𝐴 ) ∈ 𝑌 )
32 uncom ⊢ ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = ( ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ∪ { ( 𝑔 ‘ 𝐴 ) } )
33 difsnid ⊢ ( ( 𝑔 ‘ 𝐴 ) ∈ 𝑌 → ( ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ∪ { ( 𝑔 ‘ 𝐴 ) } ) = 𝑌 )
34 32 33 syl5eq ⊢ ( ( 𝑔 ‘ 𝐴 ) ∈ 𝑌 → ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = 𝑌 )
35 31 34 syl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = 𝑌 )
36 uncom ⊢ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) = ( ( 𝑌 ∖ { 𝐵 } ) ∪ { 𝐵 } )
37 difsnid ⊢ ( 𝐵 ∈ 𝑌 → ( ( 𝑌 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝑌 )
38 36 37 syl5eq ⊢ ( 𝐵 ∈ 𝑌 → ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) = 𝑌 )
39 19 38 syl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) = 𝑌 )
40 f1oeq23 ⊢ ( ( ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = 𝑌 ∧ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) = 𝑌 ) → ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) : ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) –1-1-onto→ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) ↔ ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) : 𝑌 –1-1-onto→ 𝑌 ) )
41 35 39 40 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) : ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) –1-1-onto→ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) ↔ ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) : 𝑌 –1-1-onto→ 𝑌 ) )
42 28 41 mpbid ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) : 𝑌 –1-1-onto→ 𝑌 )
43 simprl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → 𝑔 : 𝑋 –1-1-onto→ 𝑌 )
44 f1oco ⊢ ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) : 𝑌 –1-1-onto→ 𝑌 ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) : 𝑋 –1-1-onto→ 𝑌 )
45 42 43 44 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) : 𝑋 –1-1-onto→ 𝑌 )
46 f1ofn ⊢ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 → 𝑔 Fn 𝑋 )
47 46 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → 𝑔 Fn 𝑋 )
48 fvco2 ⊢ ( ( 𝑔 Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ‘ ( 𝑔 ‘ 𝐴 ) ) )
49 47 30 48 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ‘ ( 𝑔 ‘ 𝐴 ) ) )
50 f1ofn ⊢ ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } : { ( 𝑔 ‘ 𝐴 ) } –1-1-onto→ { 𝐵 } → { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } Fn { ( 𝑔 ‘ 𝐴 ) } )
51 21 50 syl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } Fn { ( 𝑔 ‘ 𝐴 ) } )
52 f1ofn ⊢ ( ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) → ℎ Fn ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) )
53 52 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ℎ Fn ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) )
54 17 snid ⊢ ( 𝑔 ‘ 𝐴 ) ∈ { ( 𝑔 ‘ 𝐴 ) }
55 54 a1i ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( 𝑔 ‘ 𝐴 ) ∈ { ( 𝑔 ‘ 𝐴 ) } )
56 fvun1 ⊢ ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } Fn { ( 𝑔 ‘ 𝐴 ) } ∧ ℎ Fn ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ∧ ( ( { ( 𝑔 ‘ 𝐴 ) } ∩ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = ∅ ∧ ( 𝑔 ‘ 𝐴 ) ∈ { ( 𝑔 ‘ 𝐴 ) } ) ) → ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ‘ ( 𝑔 ‘ 𝐴 ) ) = ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ‘ ( 𝑔 ‘ 𝐴 ) ) )
57 51 53 24 55 56 syl112anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ‘ ( 𝑔 ‘ 𝐴 ) ) = ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ‘ ( 𝑔 ‘ 𝐴 ) ) )
58 fvsng ⊢ ( ( ( 𝑔 ‘ 𝐴 ) ∈ V ∧ 𝐵 ∈ 𝑌 ) → ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ‘ ( 𝑔 ‘ 𝐴 ) ) = 𝐵 )
59 18 19 58 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ‘ ( 𝑔 ‘ 𝐴 ) ) = 𝐵 )
60 49 57 59 3eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = 𝐵 )
61 snex ⊢ { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∈ V
62 vex ⊢ ℎ ∈ V
63 61 62 unex ⊢ ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∈ V
64 vex ⊢ 𝑔 ∈ V
65 63 64 coex ⊢ ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) ∈ V
66 f1oeq1 ⊢ ( 𝑓 = ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) → ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ↔ ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) : 𝑋 –1-1-onto→ 𝑌 ) )
67 fveq1 ⊢ ( 𝑓 = ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) → ( 𝑓 ‘ 𝐴 ) = ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) )
68 67 eqeq1d ⊢ ( 𝑓 = ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) → ( ( 𝑓 ‘ 𝐴 ) = 𝐵 ↔ ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = 𝐵 ) )
69 66 68 anbi12d ⊢ ( 𝑓 = ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) → ( ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) ↔ ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) : 𝑋 –1-1-onto→ 𝑌 ∧ ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = 𝐵 ) ) )
70 65 69 spcev ⊢ ( ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) : 𝑋 –1-1-onto→ 𝑌 ∧ ( ( ( { ⟨ ( 𝑔 ‘ 𝐴 ) , 𝐵 ⟩ } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = 𝐵 ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) )
71 45 60 70 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) )
72 71 expr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ( ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) ) )
73 72 exlimdv ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ( ∃ ℎ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) ) )
74 16 73 mpd ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) )
75 3 74 exlimddv ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) )