Theorem enfixsn 8069

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

Assertion

Ref	Expression
enfixsn	|- ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) )

Distinct variable groups:   A, f   B, f   f, X   f, Y

Proof of Theorem enfixsn

Dummy variables g h are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp3 1063	. . 3 |- ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> X ~~ Y )
2		bren 7964	. . 3 |- ( X ~~ Y <-> E. g g : X -1-1-onto-> Y )
3	1, 2	sylib 208	. 2 |- ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> E. g g : X -1-1-onto-> Y )
4		relen 7960	. . . . . . . 8 |- Rel ~~
5	4	brrelex2i 5159	. . . . . . 7 |- ( X ~~ Y -> Y e. _V )
6	5	3ad2ant3 1084	. . . . . 6 |- ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> Y e. _V )
7	6	adantr 481	. . . . 5 |- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> Y e. _V )
8		f1of 6137	. . . . . . 7 |- ( g : X -1-1-onto-> Y -> g : X --> Y )
9	8	adantl 482	. . . . . 6 |- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> g : X --> Y )
10		simpl1 1064	. . . . . 6 |- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> A e. X )
11	9, 10	ffvelrnd 6360	. . . . 5 |- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> ( g ` A ) e. Y )
12		simpl2 1065	. . . . 5 |- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> B e. Y )
13		difsnen 8042	. . . . 5 |- ( ( Y e. _V /\ ( g ` A ) e. Y /\ B e. Y ) -> ( Y \ { ( g ` A ) } ) ~~ ( Y \ { B } ) )
14	7, 11, 12, 13	syl3anc 1326	. . . 4 |- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> ( Y \ { ( g ` A ) } ) ~~ ( Y \ { B } ) )
15		bren 7964	. . . 4 |- ( ( Y \ { ( g ` A ) } ) ~~ ( Y \ { B } ) <-> E. h h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) )
16	14, 15	sylib 208	. . 3 |- ( ( ( 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 6201	. . . . . . . . . . 11 |- ( g ` A ) e. _V
18	17	a1i 11	. . . . . . . . . 10 |- ( ( ( 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 1065	. . . . . . . . . 10 |- ( ( ( 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 6177	. . . . . . . . . 10 |- ( ( ( g ` A ) e. _V /\ B e. Y ) -> { <. ( g ` A ) , B >. } : { ( g ` A ) } -1-1-onto-> { B } )
21	18, 19, 20	syl2anc 693	. . . . . . . . 9 |- ( ( ( 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 796	. . . . . . . . 9 |- ( ( ( 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 4040	. . . . . . . . . 10 |- ( { ( g ` A ) } i^i ( Y \ { ( g ` A ) } ) ) = (/)
24	23	a1i 11	. . . . . . . . 9 |- ( ( ( 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 4040	. . . . . . . . . 10 |- ( { B } i^i ( Y \ { B } ) ) = (/)
26	25	a1i 11	. . . . . . . . 9 |- ( ( ( 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 6156	. . . . . . . . 9 |- ( ( ( { <. ( 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 1327	. . . . . . . 8 |- ( ( ( 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 764	. . . . . . . . . . 11 |- ( ( ( 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 1064	. . . . . . . . . . 11 |- ( ( ( 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 6360	. . . . . . . . . 10 |- ( ( ( 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 3757	. . . . . . . . . . 11 |- ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) = ( ( Y \ { ( g ` A ) } ) u. { ( g ` A ) } )
33		difsnid 4341	. . . . . . . . . . 11 |- ( ( g ` A ) e. Y -> ( ( Y \ { ( g ` A ) } ) u. { ( g ` A ) } ) = Y )
34	32, 33	syl5eq 2668	. . . . . . . . . 10 |- ( ( g ` A ) e. Y -> ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) = Y )
35	31, 34	syl 17	. . . . . . . . 9 |- ( ( ( 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 3757	. . . . . . . . . . 11 |- ( { B } u. ( Y \ { B } ) ) = ( ( Y \ { B } ) u. { B } )
37		difsnid 4341	. . . . . . . . . . 11 |- ( B e. Y -> ( ( Y \ { B } ) u. { B } ) = Y )
38	36, 37	syl5eq 2668	. . . . . . . . . 10 |- ( B e. Y -> ( { B } u. ( Y \ { B } ) ) = Y )
39	19, 38	syl 17	. . . . . . . . 9 |- ( ( ( 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 6130	. . . . . . . . 9 |- ( ( ( { ( 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 693	. . . . . . . 8 |- ( ( ( 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 222	. . . . . . 7 |- ( ( ( 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 794	. . . . . . 7 |- ( ( ( 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 6159	. . . . . . 7 |- ( ( ( { <. ( 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 693	. . . . . 6 |- ( ( ( 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 6138	. . . . . . . . 9 |- ( g : X -1-1-onto-> Y -> g Fn X )
47	46	ad2antrl 764	. . . . . . . 8 |- ( ( ( 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 6273	. . . . . . . 8 |- ( ( 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 693	. . . . . . 7 |- ( ( ( 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 6138	. . . . . . . . 9 |- ( { <. ( g ` A ) , B >. } : { ( g ` A ) } -1-1-onto-> { B } -> { <. ( g ` A ) , B >. } Fn { ( g ` A ) } )
51	21, 50	syl 17	. . . . . . . 8 |- ( ( ( 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 6138	. . . . . . . . 9 |- ( h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) -> h Fn ( Y \ { ( g ` A ) } ) )
53	52	ad2antll 765	. . . . . . . 8 |- ( ( ( 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 4208	. . . . . . . . 9 |- ( g ` A ) e. { ( g ` A ) }
55	54	a1i 11	. . . . . . . 8 |- ( ( ( 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 6269	. . . . . . . 8 |- ( ( { <. ( 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 1330	. . . . . . 7 |- ( ( ( 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 6447	. . . . . . . 8 |- ( ( ( g ` A ) e. _V /\ B e. Y ) -> ( { <. ( g ` A ) , B >. } ` ( g ` A ) ) = B )
59	18, 19, 58	syl2anc 693	. . . . . . 7 |- ( ( ( 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 2660	. . . . . 6 |- ( ( ( 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 4908	. . . . . . . . 9 |- { <. ( g ` A ) , B >. } e. _V
62		vex 3203	. . . . . . . . 9 |- h e. _V
63	61, 62	unex 6956	. . . . . . . 8 |- ( { <. ( g ` A ) , B >. } u. h ) e. _V
64		vex 3203	. . . . . . . 8 |- g e. _V
65	63, 64	coex 7118	. . . . . . 7 |- ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) e. _V
66		f1oeq1 6127	. . . . . . . 8 |- ( 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 6190	. . . . . . . . 9 |- ( f = ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) -> ( f ` A ) = ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) )
68	67	eqeq1d 2624	. . . . . . . 8 |- ( f = ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) -> ( ( f ` A ) = B <-> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = B ) )
69	66, 68	anbi12d 747	. . . . . . 7 |- ( 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 3300	. . . . . 6 |- ( ( ( ( { <. ( 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 693	. . . . 5 |- ( ( ( 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 643	. . . 4 |- ( ( ( 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 1861	. . 3 |- ( ( ( 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 15	. 2 |- ( ( ( 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 1863	1 |- ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   (/)c0 3915   {csn 4177   <.cop 4183   class class class wbr 4653   o. ccom 5118   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888   ~~ cen 7952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-1o 7560  df-er 7742  df-en 7956

This theorem is referenced by:  mapfien2  8314