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 
|- ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> X ~~ Y )
2 bren 
 |-  ( X ~~ Y <-> E. g g : X -1-1-onto-> Y )
3 1 2 sylib 
 |-  ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> E. g g : X -1-1-onto-> Y )
4 relen 
 |-  Rel ~~
5 4 brrelex2i 
 |-  ( X ~~ Y -> Y e. _V )
6 5 3ad2ant3 
 |-  ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> Y e. _V )
7 6 adantr 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> Y e. _V )
8 f1of 
 |-  ( g : X -1-1-onto-> Y -> g : X --> Y )
9 8 adantl 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> g : X --> Y )
10 simpl1 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> A e. X )
11 9 10 ffvelrnd 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> ( g ` A ) e. Y )
12 simpl2 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> B e. Y )
13 difsnen 
 |-  ( ( Y e. _V /\ ( g ` A ) e. Y /\ B e. Y ) -> ( Y \ { ( g ` A ) } ) ~~ ( Y \ { B } ) )
14 7 11 12 13 syl3anc 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> ( Y \ { ( g ` A ) } ) ~~ ( Y \ { B } ) )
15 bren 
 |-  ( ( Y \ { ( g ` A ) } ) ~~ ( Y \ { B } ) <-> E. h h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) )
16 14 15 sylib 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> E. h h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) )
17 fvex 
 |-  ( g ` A ) e. _V
18 17 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( g ` A ) e. _V )
19 simpl2 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> B e. Y )
20 f1osng 
 |-  ( ( ( g ` A ) e. _V /\ B e. Y ) -> { <. ( g ` A ) , B >. } : { ( g ` A ) } -1-1-onto-> { B } )
21 18 19 20 syl2anc 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> { <. ( g ` A ) , B >. } : { ( g ` A ) } -1-1-onto-> { B } )
22 simprr 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) )
23 disjdif 
 |-  ( { ( g ` A ) } i^i ( Y \ { ( g ` A ) } ) ) = (/)
24 23 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { ( g ` A ) } i^i ( Y \ { ( g ` A ) } ) ) = (/) )
25 disjdif 
 |-  ( { B } i^i ( Y \ { B } ) ) = (/)
26 25 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { B } i^i ( Y \ { B } ) ) = (/) )
27 f1oun 
 |-  ( ( ( { <. ( g ` A ) , B >. } : { ( g ` A ) } -1-1-onto-> { B } /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) /\ ( ( { ( g ` A ) } i^i ( Y \ { ( g ` A ) } ) ) = (/) /\ ( { B } i^i ( Y \ { B } ) ) = (/) ) ) -> ( { <. ( g ` A ) , B >. } u. h ) : ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) -1-1-onto-> ( { B } u. ( Y \ { B } ) ) )
28 21 22 24 26 27 syl22anc 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { <. ( g ` A ) , B >. } u. h ) : ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) -1-1-onto-> ( { B } u. ( Y \ { B } ) ) )
29 8 ad2antrl 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> g : X --> Y )
30 simpl1 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> A e. X )
31 29 30 ffvelrnd 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( g ` A ) e. Y )
32 uncom 
 |-  ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) = ( ( Y \ { ( g ` A ) } ) u. { ( g ` A ) } )
33 difsnid 
 |-  ( ( g ` A ) e. Y -> ( ( Y \ { ( g ` A ) } ) u. { ( g ` A ) } ) = Y )
34 32 33 syl5eq 
 |-  ( ( g ` A ) e. Y -> ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) = Y )
35 31 34 syl 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) = Y )
36 uncom 
 |-  ( { B } u. ( Y \ { B } ) ) = ( ( Y \ { B } ) u. { B } )
37 difsnid 
 |-  ( B e. Y -> ( ( Y \ { B } ) u. { B } ) = Y )
38 36 37 syl5eq 
 |-  ( B e. Y -> ( { B } u. ( Y \ { B } ) ) = Y )
39 19 38 syl 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { B } u. ( Y \ { B } ) ) = Y )
40 f1oeq23 
 |-  ( ( ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) = Y /\ ( { B } u. ( Y \ { B } ) ) = Y ) -> ( ( { <. ( g ` A ) , B >. } u. h ) : ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) -1-1-onto-> ( { B } u. ( Y \ { B } ) ) <-> ( { <. ( g ` A ) , B >. } u. h ) : Y -1-1-onto-> Y ) )
41 35 39 40 syl2anc 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( ( { <. ( g ` A ) , B >. } u. h ) : ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) -1-1-onto-> ( { B } u. ( Y \ { B } ) ) <-> ( { <. ( g ` A ) , B >. } u. h ) : Y -1-1-onto-> Y ) )
42 28 41 mpbid 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { <. ( g ` A ) , B >. } u. h ) : Y -1-1-onto-> Y )
43 simprl 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> g : X -1-1-onto-> Y )
44 f1oco 
 |-  ( ( ( { <. ( g ` A ) , B >. } u. h ) : Y -1-1-onto-> Y /\ g : X -1-1-onto-> Y ) -> ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) : X -1-1-onto-> Y )
45 42 43 44 syl2anc 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) : X -1-1-onto-> Y )
46 f1ofn 
 |-  ( g : X -1-1-onto-> Y -> g Fn X )
47 46 ad2antrl 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> g Fn X )
48 fvco2 
 |-  ( ( g Fn X /\ A e. X ) -> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = ( ( { <. ( g ` A ) , B >. } u. h ) ` ( g ` A ) ) )
49 47 30 48 syl2anc 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = ( ( { <. ( g ` A ) , B >. } u. h ) ` ( g ` A ) ) )
50 f1ofn 
 |-  ( { <. ( g ` A ) , B >. } : { ( g ` A ) } -1-1-onto-> { B } -> { <. ( g ` A ) , B >. } Fn { ( g ` A ) } )
51 21 50 syl 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> { <. ( g ` A ) , B >. } Fn { ( g ` A ) } )
52 f1ofn 
 |-  ( h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) -> h Fn ( Y \ { ( g ` A ) } ) )
53 52 ad2antll 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> h Fn ( Y \ { ( g ` A ) } ) )
54 17 snid 
 |-  ( g ` A ) e. { ( g ` A ) }
55 54 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( g ` A ) e. { ( g ` A ) } )
56 fvun1 
 |-  ( ( { <. ( g ` A ) , B >. } Fn { ( g ` A ) } /\ h Fn ( Y \ { ( g ` A ) } ) /\ ( ( { ( g ` A ) } i^i ( Y \ { ( g ` A ) } ) ) = (/) /\ ( g ` A ) e. { ( g ` A ) } ) ) -> ( ( { <. ( g ` A ) , B >. } u. h ) ` ( g ` A ) ) = ( { <. ( g ` A ) , B >. } ` ( g ` A ) ) )
57 51 53 24 55 56 syl112anc 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( ( { <. ( g ` A ) , B >. } u. h ) ` ( g ` A ) ) = ( { <. ( g ` A ) , B >. } ` ( g ` A ) ) )
58 fvsng 
 |-  ( ( ( g ` A ) e. _V /\ B e. Y ) -> ( { <. ( g ` A ) , B >. } ` ( g ` A ) ) = B )
59 18 19 58 syl2anc 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { <. ( g ` A ) , B >. } ` ( g ` A ) ) = B )
60 49 57 59 3eqtrd 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = B )
61 snex 
 |-  { <. ( g ` A ) , B >. } e. _V
62 vex 
 |-  h e. _V
63 61 62 unex 
 |-  ( { <. ( g ` A ) , B >. } u. h ) e. _V
64 vex 
 |-  g e. _V
65 63 64 coex 
 |-  ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) e. _V
66 f1oeq1 
 |-  ( f = ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) -> ( f : X -1-1-onto-> Y <-> ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) : X -1-1-onto-> Y ) )
67 fveq1 
 |-  ( f = ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) -> ( f ` A ) = ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) )
68 67 eqeq1d 
 |-  ( f = ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) -> ( ( f ` A ) = B <-> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = B ) )
69 66 68 anbi12d 
 |-  ( f = ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) -> ( ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) <-> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) : X -1-1-onto-> Y /\ ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = B ) ) )
70 65 69 spcev 
 |-  ( ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) : X -1-1-onto-> Y /\ ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = B ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) )
71 45 60 70 syl2anc 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) )
72 71 expr 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> ( h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) ) )
73 72 exlimdv 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> ( E. h h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) ) )
74 16 73 mpd 
 |-  ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) )
75 3 74 exlimddv 
 |-  ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) )