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 eqtrid ( ( 𝑔𝐴 ) ∈ 𝑌 → ( { ( 𝑔𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔𝐴 ) } ) ) = 𝑌 )
35 31 34 syl ( ( ( 𝐴𝑋𝐵𝑌𝑋𝑌 ) ∧ ( 𝑔 : 𝑋1-1-onto𝑌 : ( 𝑌 ∖ { ( 𝑔𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { ( 𝑔𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔𝐴 ) } ) ) = 𝑌 )
36 uncom ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) = ( ( 𝑌 ∖ { 𝐵 } ) ∪ { 𝐵 } )
37 difsnid ( 𝐵𝑌 → ( ( 𝑌 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝑌 )
38 36 37 eqtrid ( 𝐵𝑌 → ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) = 𝑌 )
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𝑌 ∧ ( 𝑓𝐴 ) = 𝐵 ) )