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 eqtrid
 |-  ( ( 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 eqtrid
 |-  ( 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 ) )