symgtgp

Description: The symmetric group is a topological group. (Contributed by Mario Carneiro, 2-Sep-2015) (Proof shortened by AV, 30-Mar-2024)

		Ref	Expression
	Hypothesis	symgtgp.g	\|- G = ( SymGrp ` A )
	Assertion	symgtgp	\|- ( A e. V -> G e. TopGrp )

Proof

Step	Hyp	Ref	Expression
1		symgtgp.g	\|- G = ( SymGrp ` A )
2	1	symggrp	\|- ( A e. V -> G e. Grp )
3		eqid	\|- ( EndoFMnd ` A ) = ( EndoFMnd ` A )
4	3	efmndtmd	\|- ( A e. V -> ( EndoFMnd ` A ) e. TopMnd )
5		eqid	\|- ( Base ` G ) = ( Base ` G )
6	3 1 5	symgsubmefmnd	\|- ( A e. V -> ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) )
7	1 5 3	symgressbas	\|- G = ( ( EndoFMnd ` A ) \|`s ( Base ` G ) )
8	7	submtmd	\|- ( ( ( EndoFMnd ` A ) e. TopMnd /\ ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) ) -> G e. TopMnd )
9	4 6 8	syl2anc	\|- ( A e. V -> G e. TopMnd )
10		eqid	\|- ( Xt_ ` ( A X. { ~P A } ) ) = ( Xt_ ` ( A X. { ~P A } ) )
11	1 5	symgtopn	\|- ( A e. V -> ( ( Xt_ ` ( A X. { ~P A } ) ) \|`t ( Base ` G ) ) = ( TopOpen ` G ) )
12		distopon	\|- ( A e. V -> ~P A e. ( TopOn ` A ) )
13	10	pttoponconst	\|- ( ( A e. V /\ ~P A e. ( TopOn ` A ) ) -> ( Xt_ ` ( A X. { ~P A } ) ) e. ( TopOn ` ( A ^m A ) ) )
14	12 13	mpdan	\|- ( A e. V -> ( Xt_ ` ( A X. { ~P A } ) ) e. ( TopOn ` ( A ^m A ) ) )
15	1 5	elsymgbas	\|- ( A e. V -> ( x e. ( Base ` G ) <-> x : A -1-1-onto-> A ) )
16		f1of	\|- ( x : A -1-1-onto-> A -> x : A --> A )
17		elmapg	\|- ( ( A e. V /\ A e. V ) -> ( x e. ( A ^m A ) <-> x : A --> A ) )
18	17	anidms	\|- ( A e. V -> ( x e. ( A ^m A ) <-> x : A --> A ) )
19	16 18	imbitrrid	\|- ( A e. V -> ( x : A -1-1-onto-> A -> x e. ( A ^m A ) ) )
20	15 19	sylbid	\|- ( A e. V -> ( x e. ( Base ` G ) -> x e. ( A ^m A ) ) )
21	20	ssrdv	\|- ( A e. V -> ( Base ` G ) C_ ( A ^m A ) )
22		resttopon	\|- ( ( ( Xt_ ` ( A X. { ~P A } ) ) e. ( TopOn ` ( A ^m A ) ) /\ ( Base ` G ) C_ ( A ^m A ) ) -> ( ( Xt_ ` ( A X. { ~P A } ) ) \|`t ( Base ` G ) ) e. ( TopOn ` ( Base ` G ) ) )
23	14 21 22	syl2anc	\|- ( A e. V -> ( ( Xt_ ` ( A X. { ~P A } ) ) \|`t ( Base ` G ) ) e. ( TopOn ` ( Base ` G ) ) )
24	11 23	eqeltrrd	\|- ( A e. V -> ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) )
25		id	\|- ( A e. V -> A e. V )
26		distop	\|- ( A e. V -> ~P A e. Top )
27		fconst6g	\|- ( ~P A e. Top -> ( A X. { ~P A } ) : A --> Top )
28	26 27	syl	\|- ( A e. V -> ( A X. { ~P A } ) : A --> Top )
29	15	biimpa	\|- ( ( A e. V /\ x e. ( Base ` G ) ) -> x : A -1-1-onto-> A )
30		f1ocnv	\|- ( x : A -1-1-onto-> A -> `' x : A -1-1-onto-> A )
31		f1of	\|- ( `' x : A -1-1-onto-> A -> `' x : A --> A )
32	29 30 31	3syl	\|- ( ( A e. V /\ x e. ( Base ` G ) ) -> `' x : A --> A )
33	32	ffvelcdmda	\|- ( ( ( A e. V /\ x e. ( Base ` G ) ) /\ y e. A ) -> ( `' x ` y ) e. A )
34	33	an32s	\|- ( ( ( A e. V /\ y e. A ) /\ x e. ( Base ` G ) ) -> ( `' x ` y ) e. A )
35	34	fmpttd	\|- ( ( A e. V /\ y e. A ) -> ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) : ( Base ` G ) --> A )
36	35	adantr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) : ( Base ` G ) --> A )
37		cnveq	\|- ( x = f -> `' x = `' f )
38	37	fveq1d	\|- ( x = f -> ( `' x ` y ) = ( `' f ` y ) )
39		eqid	\|- ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) = ( x e. ( Base ` G ) \|-> ( `' x ` y ) )
40		fvex	\|- ( `' f ` y ) e. _V
41	38 39 40	fvmpt	\|- ( f e. ( Base ` G ) -> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) ` f ) = ( `' f ` y ) )
42	41	ad2antlr	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ t e. ~P A ) -> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) ` f ) = ( `' f ` y ) )
43	42	eleq1d	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ t e. ~P A ) -> ( ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) ` f ) e. t <-> ( `' f ` y ) e. t ) )
44		eqid	\|- ( u e. ( Base ` G ) \|-> ( u ` ( `' f ` y ) ) ) = ( u e. ( Base ` G ) \|-> ( u ` ( `' f ` y ) ) )
45	44	mptiniseg	\|- ( y e. _V -> ( `' ( u e. ( Base ` G ) \|-> ( u ` ( `' f ` y ) ) ) " { y } ) = { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } )
46	45	elv	\|- ( `' ( u e. ( Base ` G ) \|-> ( u ` ( `' f ` y ) ) ) " { y } ) = { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y }
47		eqid	\|- ( ( Xt_ ` ( A X. { ~P A } ) ) \|`t ( Base ` G ) ) = ( ( Xt_ ` ( A X. { ~P A } ) ) \|`t ( Base ` G ) )
48	14	ad2antrr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( Xt_ ` ( A X. { ~P A } ) ) e. ( TopOn ` ( A ^m A ) ) )
49	21	ad2antrr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( Base ` G ) C_ ( A ^m A ) )
50		toponuni	\|- ( ( Xt_ ` ( A X. { ~P A } ) ) e. ( TopOn ` ( A ^m A ) ) -> ( A ^m A ) = U. ( Xt_ ` ( A X. { ~P A } ) ) )
51		mpteq1	\|- ( ( A ^m A ) = U. ( Xt_ ` ( A X. { ~P A } ) ) -> ( u e. ( A ^m A ) \|-> ( u ` ( `' f ` y ) ) ) = ( u e. U. ( Xt_ ` ( A X. { ~P A } ) ) \|-> ( u ` ( `' f ` y ) ) ) )
52	48 50 51	3syl	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( u e. ( A ^m A ) \|-> ( u ` ( `' f ` y ) ) ) = ( u e. U. ( Xt_ ` ( A X. { ~P A } ) ) \|-> ( u ` ( `' f ` y ) ) ) )
53		simpll	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> A e. V )
54	28	ad2antrr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( A X. { ~P A } ) : A --> Top )
55	1 5	elsymgbas	\|- ( A e. V -> ( f e. ( Base ` G ) <-> f : A -1-1-onto-> A ) )
56	55	adantr	\|- ( ( A e. V /\ y e. A ) -> ( f e. ( Base ` G ) <-> f : A -1-1-onto-> A ) )
57	56	biimpa	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> f : A -1-1-onto-> A )
58		f1ocnv	\|- ( f : A -1-1-onto-> A -> `' f : A -1-1-onto-> A )
59		f1of	\|- ( `' f : A -1-1-onto-> A -> `' f : A --> A )
60	57 58 59	3syl	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> `' f : A --> A )
61		simplr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> y e. A )
62	60 61	ffvelcdmd	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( `' f ` y ) e. A )
63		eqid	\|- U. ( Xt_ ` ( A X. { ~P A } ) ) = U. ( Xt_ ` ( A X. { ~P A } ) )
64	63 10	ptpjcn	\|- ( ( A e. V /\ ( A X. { ~P A } ) : A --> Top /\ ( `' f ` y ) e. A ) -> ( u e. U. ( Xt_ ` ( A X. { ~P A } ) ) \|-> ( u ` ( `' f ` y ) ) ) e. ( ( Xt_ ` ( A X. { ~P A } ) ) Cn ( ( A X. { ~P A } ) ` ( `' f ` y ) ) ) )
65	53 54 62 64	syl3anc	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( u e. U. ( Xt_ ` ( A X. { ~P A } ) ) \|-> ( u ` ( `' f ` y ) ) ) e. ( ( Xt_ ` ( A X. { ~P A } ) ) Cn ( ( A X. { ~P A } ) ` ( `' f ` y ) ) ) )
66	26	ad2antrr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ~P A e. Top )
67		fvconst2g	\|- ( ( ~P A e. Top /\ ( `' f ` y ) e. A ) -> ( ( A X. { ~P A } ) ` ( `' f ` y ) ) = ~P A )
68	66 62 67	syl2anc	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( ( A X. { ~P A } ) ` ( `' f ` y ) ) = ~P A )
69	68	oveq2d	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( ( Xt_ ` ( A X. { ~P A } ) ) Cn ( ( A X. { ~P A } ) ` ( `' f ` y ) ) ) = ( ( Xt_ ` ( A X. { ~P A } ) ) Cn ~P A ) )
70	65 69	eleqtrd	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( u e. U. ( Xt_ ` ( A X. { ~P A } ) ) \|-> ( u ` ( `' f ` y ) ) ) e. ( ( Xt_ ` ( A X. { ~P A } ) ) Cn ~P A ) )
71	52 70	eqeltrd	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( u e. ( A ^m A ) \|-> ( u ` ( `' f ` y ) ) ) e. ( ( Xt_ ` ( A X. { ~P A } ) ) Cn ~P A ) )
72	47 48 49 71	cnmpt1res	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( u e. ( Base ` G ) \|-> ( u ` ( `' f ` y ) ) ) e. ( ( ( Xt_ ` ( A X. { ~P A } ) ) \|`t ( Base ` G ) ) Cn ~P A ) )
73	11	oveq1d	\|- ( A e. V -> ( ( ( Xt_ ` ( A X. { ~P A } ) ) \|`t ( Base ` G ) ) Cn ~P A ) = ( ( TopOpen ` G ) Cn ~P A ) )
74	73	ad2antrr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( ( ( Xt_ ` ( A X. { ~P A } ) ) \|`t ( Base ` G ) ) Cn ~P A ) = ( ( TopOpen ` G ) Cn ~P A ) )
75	72 74	eleqtrd	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( u e. ( Base ` G ) \|-> ( u ` ( `' f ` y ) ) ) e. ( ( TopOpen ` G ) Cn ~P A ) )
76		snelpwi	\|- ( y e. A -> { y } e. ~P A )
77	76	ad2antlr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> { y } e. ~P A )
78		cnima	\|- ( ( ( u e. ( Base ` G ) \|-> ( u ` ( `' f ` y ) ) ) e. ( ( TopOpen ` G ) Cn ~P A ) /\ { y } e. ~P A ) -> ( `' ( u e. ( Base ` G ) \|-> ( u ` ( `' f ` y ) ) ) " { y } ) e. ( TopOpen ` G ) )
79	75 77 78	syl2anc	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( `' ( u e. ( Base ` G ) \|-> ( u ` ( `' f ` y ) ) ) " { y } ) e. ( TopOpen ` G ) )
80	46 79	eqeltrrid	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } e. ( TopOpen ` G ) )
81	80	adantr	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } e. ( TopOpen ` G ) )
82		fveq1	\|- ( u = f -> ( u ` ( `' f ` y ) ) = ( f ` ( `' f ` y ) ) )
83	82	eqeq1d	\|- ( u = f -> ( ( u ` ( `' f ` y ) ) = y <-> ( f ` ( `' f ` y ) ) = y ) )
84		simplr	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> f e. ( Base ` G ) )
85	57	adantr	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> f : A -1-1-onto-> A )
86		simpllr	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> y e. A )
87		f1ocnvfv2	\|- ( ( f : A -1-1-onto-> A /\ y e. A ) -> ( f ` ( `' f ` y ) ) = y )
88	85 86 87	syl2anc	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> ( f ` ( `' f ` y ) ) = y )
89	83 84 88	elrabd	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> f e. { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } )
90		ssrab2	\|- { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } C_ ( Base ` G )
91	90	a1i	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } C_ ( Base ` G ) )
92	15	ad3antrrr	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> ( x e. ( Base ` G ) <-> x : A -1-1-onto-> A ) )
93	92	biimpa	\|- ( ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) /\ x e. ( Base ` G ) ) -> x : A -1-1-onto-> A )
94	62	ad2antrr	\|- ( ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) /\ x e. ( Base ` G ) ) -> ( `' f ` y ) e. A )
95		f1ocnvfv	\|- ( ( x : A -1-1-onto-> A /\ ( `' f ` y ) e. A ) -> ( ( x ` ( `' f ` y ) ) = y -> ( `' x ` y ) = ( `' f ` y ) ) )
96	93 94 95	syl2anc	\|- ( ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) /\ x e. ( Base ` G ) ) -> ( ( x ` ( `' f ` y ) ) = y -> ( `' x ` y ) = ( `' f ` y ) ) )
97		simplrr	\|- ( ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) /\ x e. ( Base ` G ) ) -> ( `' f ` y ) e. t )
98		eleq1	\|- ( ( `' x ` y ) = ( `' f ` y ) -> ( ( `' x ` y ) e. t <-> ( `' f ` y ) e. t ) )
99	97 98	syl5ibrcom	\|- ( ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) /\ x e. ( Base ` G ) ) -> ( ( `' x ` y ) = ( `' f ` y ) -> ( `' x ` y ) e. t ) )
100	96 99	syld	\|- ( ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) /\ x e. ( Base ` G ) ) -> ( ( x ` ( `' f ` y ) ) = y -> ( `' x ` y ) e. t ) )
101	100	ralrimiva	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> A. x e. ( Base ` G ) ( ( x ` ( `' f ` y ) ) = y -> ( `' x ` y ) e. t ) )
102		fveq1	\|- ( u = x -> ( u ` ( `' f ` y ) ) = ( x ` ( `' f ` y ) ) )
103	102	eqeq1d	\|- ( u = x -> ( ( u ` ( `' f ` y ) ) = y <-> ( x ` ( `' f ` y ) ) = y ) )
104	103	ralrab	\|- ( A. x e. { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ( `' x ` y ) e. t <-> A. x e. ( Base ` G ) ( ( x ` ( `' f ` y ) ) = y -> ( `' x ` y ) e. t ) )
105	101 104	sylibr	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> A. x e. { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ( `' x ` y ) e. t )
106		ssrab	\|- ( { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } C_ { x e. ( Base ` G ) \| ( `' x ` y ) e. t } <-> ( { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } C_ ( Base ` G ) /\ A. x e. { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ( `' x ` y ) e. t ) )
107	91 105 106	sylanbrc	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } C_ { x e. ( Base ` G ) \| ( `' x ` y ) e. t } )
108	39	mptpreima	\|- ( `' ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " t ) = { x e. ( Base ` G ) \| ( `' x ` y ) e. t }
109	107 108	sseqtrrdi	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } C_ ( `' ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " t ) )
110		funmpt	\|- Fun ( x e. ( Base ` G ) \|-> ( `' x ` y ) )
111		fvex	\|- ( `' x ` y ) e. _V
112	111 39	dmmpti	\|- dom ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) = ( Base ` G )
113	91 112	sseqtrrdi	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } C_ dom ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) )
114		funimass3	\|- ( ( Fun ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) /\ { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } C_ dom ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) ) -> ( ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ) C_ t <-> { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } C_ ( `' ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " t ) ) )
115	110 113 114	sylancr	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> ( ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ) C_ t <-> { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } C_ ( `' ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " t ) ) )
116	109 115	mpbird	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ) C_ t )
117		eleq2	\|- ( v = { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } -> ( f e. v <-> f e. { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ) )
118		imaeq2	\|- ( v = { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } -> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " v ) = ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ) )
119	118	sseq1d	\|- ( v = { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } -> ( ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " v ) C_ t <-> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ) C_ t ) )
120	117 119	anbi12d	\|- ( v = { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } -> ( ( f e. v /\ ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " v ) C_ t ) <-> ( f e. { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } /\ ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ) C_ t ) ) )
121	120	rspcev	\|- ( ( { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } e. ( TopOpen ` G ) /\ ( f e. { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } /\ ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " { u e. ( Base ` G ) \| ( u ` ( `' f ` y ) ) = y } ) C_ t ) ) -> E. v e. ( TopOpen ` G ) ( f e. v /\ ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " v ) C_ t ) )
122	81 89 116 121	syl12anc	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ ( t e. ~P A /\ ( `' f ` y ) e. t ) ) -> E. v e. ( TopOpen ` G ) ( f e. v /\ ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " v ) C_ t ) )
123	122	expr	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ t e. ~P A ) -> ( ( `' f ` y ) e. t -> E. v e. ( TopOpen ` G ) ( f e. v /\ ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " v ) C_ t ) ) )
124	43 123	sylbid	\|- ( ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) /\ t e. ~P A ) -> ( ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) ` f ) e. t -> E. v e. ( TopOpen ` G ) ( f e. v /\ ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " v ) C_ t ) ) )
125	124	ralrimiva	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> A. t e. ~P A ( ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) ` f ) e. t -> E. v e. ( TopOpen ` G ) ( f e. v /\ ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " v ) C_ t ) ) )
126	24	ad2antrr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) )
127	12	ad2antrr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ~P A e. ( TopOn ` A ) )
128		simpr	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> f e. ( Base ` G ) )
129		iscnp	\|- ( ( ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) /\ ~P A e. ( TopOn ` A ) /\ f e. ( Base ` G ) ) -> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( ( TopOpen ` G ) CnP ~P A ) ` f ) <-> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) : ( Base ` G ) --> A /\ A. t e. ~P A ( ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) ` f ) e. t -> E. v e. ( TopOpen ` G ) ( f e. v /\ ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " v ) C_ t ) ) ) ) )
130	126 127 128 129	syl3anc	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( ( TopOpen ` G ) CnP ~P A ) ` f ) <-> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) : ( Base ` G ) --> A /\ A. t e. ~P A ( ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) ` f ) e. t -> E. v e. ( TopOpen ` G ) ( f e. v /\ ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) " v ) C_ t ) ) ) ) )
131	36 125 130	mpbir2and	\|- ( ( ( A e. V /\ y e. A ) /\ f e. ( Base ` G ) ) -> ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( ( TopOpen ` G ) CnP ~P A ) ` f ) )
132	131	ralrimiva	\|- ( ( A e. V /\ y e. A ) -> A. f e. ( Base ` G ) ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( ( TopOpen ` G ) CnP ~P A ) ` f ) )
133		cncnp	\|- ( ( ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) /\ ~P A e. ( TopOn ` A ) ) -> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( TopOpen ` G ) Cn ~P A ) <-> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) : ( Base ` G ) --> A /\ A. f e. ( Base ` G ) ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( ( TopOpen ` G ) CnP ~P A ) ` f ) ) ) )
134	24 12 133	syl2anc	\|- ( A e. V -> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( TopOpen ` G ) Cn ~P A ) <-> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) : ( Base ` G ) --> A /\ A. f e. ( Base ` G ) ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( ( TopOpen ` G ) CnP ~P A ) ` f ) ) ) )
135	134	adantr	\|- ( ( A e. V /\ y e. A ) -> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( TopOpen ` G ) Cn ~P A ) <-> ( ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) : ( Base ` G ) --> A /\ A. f e. ( Base ` G ) ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( ( TopOpen ` G ) CnP ~P A ) ` f ) ) ) )
136	35 132 135	mpbir2and	\|- ( ( A e. V /\ y e. A ) -> ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( TopOpen ` G ) Cn ~P A ) )
137		fvconst2g	\|- ( ( ~P A e. Top /\ y e. A ) -> ( ( A X. { ~P A } ) ` y ) = ~P A )
138	26 137	sylan	\|- ( ( A e. V /\ y e. A ) -> ( ( A X. { ~P A } ) ` y ) = ~P A )
139	138	oveq2d	\|- ( ( A e. V /\ y e. A ) -> ( ( TopOpen ` G ) Cn ( ( A X. { ~P A } ) ` y ) ) = ( ( TopOpen ` G ) Cn ~P A ) )
140	136 139	eleqtrrd	\|- ( ( A e. V /\ y e. A ) -> ( x e. ( Base ` G ) \|-> ( `' x ` y ) ) e. ( ( TopOpen ` G ) Cn ( ( A X. { ~P A } ) ` y ) ) )
141	10 24 25 28 140	ptcn	\|- ( A e. V -> ( x e. ( Base ` G ) \|-> ( y e. A \|-> ( `' x ` y ) ) ) e. ( ( TopOpen ` G ) Cn ( Xt_ ` ( A X. { ~P A } ) ) ) )
142		eqid	\|- ( invg ` G ) = ( invg ` G )
143	5 142	grpinvf	\|- ( G e. Grp -> ( invg ` G ) : ( Base ` G ) --> ( Base ` G ) )
144	2 143	syl	\|- ( A e. V -> ( invg ` G ) : ( Base ` G ) --> ( Base ` G ) )
145	144	feqmptd	\|- ( A e. V -> ( invg ` G ) = ( x e. ( Base ` G ) \|-> ( ( invg ` G ) ` x ) ) )
146	1 5 142	symginv	\|- ( x e. ( Base ` G ) -> ( ( invg ` G ) ` x ) = `' x )
147	146	adantl	\|- ( ( A e. V /\ x e. ( Base ` G ) ) -> ( ( invg ` G ) ` x ) = `' x )
148	32	feqmptd	\|- ( ( A e. V /\ x e. ( Base ` G ) ) -> `' x = ( y e. A \|-> ( `' x ` y ) ) )
149	147 148	eqtrd	\|- ( ( A e. V /\ x e. ( Base ` G ) ) -> ( ( invg ` G ) ` x ) = ( y e. A \|-> ( `' x ` y ) ) )
150	149	mpteq2dva	\|- ( A e. V -> ( x e. ( Base ` G ) \|-> ( ( invg ` G ) ` x ) ) = ( x e. ( Base ` G ) \|-> ( y e. A \|-> ( `' x ` y ) ) ) )
151	145 150	eqtrd	\|- ( A e. V -> ( invg ` G ) = ( x e. ( Base ` G ) \|-> ( y e. A \|-> ( `' x ` y ) ) ) )
152		xkopt	\|- ( ( ~P A e. Top /\ A e. V ) -> ( ~P A ^ko ~P A ) = ( Xt_ ` ( A X. { ~P A } ) ) )
153	26 152	mpancom	\|- ( A e. V -> ( ~P A ^ko ~P A ) = ( Xt_ ` ( A X. { ~P A } ) ) )
154	153	oveq2d	\|- ( A e. V -> ( ( TopOpen ` G ) Cn ( ~P A ^ko ~P A ) ) = ( ( TopOpen ` G ) Cn ( Xt_ ` ( A X. { ~P A } ) ) ) )
155	141 151 154	3eltr4d	\|- ( A e. V -> ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( ~P A ^ko ~P A ) ) )
156		eqid	\|- ( ~P A ^ko ~P A ) = ( ~P A ^ko ~P A )
157	156	xkotopon	\|- ( ( ~P A e. Top /\ ~P A e. Top ) -> ( ~P A ^ko ~P A ) e. ( TopOn ` ( ~P A Cn ~P A ) ) )
158	26 26 157	syl2anc	\|- ( A e. V -> ( ~P A ^ko ~P A ) e. ( TopOn ` ( ~P A Cn ~P A ) ) )
159		frn	\|- ( ( invg ` G ) : ( Base ` G ) --> ( Base ` G ) -> ran ( invg ` G ) C_ ( Base ` G ) )
160	2 143 159	3syl	\|- ( A e. V -> ran ( invg ` G ) C_ ( Base ` G ) )
161		cndis	\|- ( ( A e. V /\ ~P A e. ( TopOn ` A ) ) -> ( ~P A Cn ~P A ) = ( A ^m A ) )
162	12 161	mpdan	\|- ( A e. V -> ( ~P A Cn ~P A ) = ( A ^m A ) )
163	21 162	sseqtrrd	\|- ( A e. V -> ( Base ` G ) C_ ( ~P A Cn ~P A ) )
164		cnrest2	\|- ( ( ( ~P A ^ko ~P A ) e. ( TopOn ` ( ~P A Cn ~P A ) ) /\ ran ( invg ` G ) C_ ( Base ` G ) /\ ( Base ` G ) C_ ( ~P A Cn ~P A ) ) -> ( ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( ~P A ^ko ~P A ) ) <-> ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( ( ~P A ^ko ~P A ) \|`t ( Base ` G ) ) ) ) )
165	158 160 163 164	syl3anc	\|- ( A e. V -> ( ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( ~P A ^ko ~P A ) ) <-> ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( ( ~P A ^ko ~P A ) \|`t ( Base ` G ) ) ) ) )
166	155 165	mpbid	\|- ( A e. V -> ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( ( ~P A ^ko ~P A ) \|`t ( Base ` G ) ) ) )
167	153	oveq1d	\|- ( A e. V -> ( ( ~P A ^ko ~P A ) \|`t ( Base ` G ) ) = ( ( Xt_ ` ( A X. { ~P A } ) ) \|`t ( Base ` G ) ) )
168	167 11	eqtrd	\|- ( A e. V -> ( ( ~P A ^ko ~P A ) \|`t ( Base ` G ) ) = ( TopOpen ` G ) )
169	168	oveq2d	\|- ( A e. V -> ( ( TopOpen ` G ) Cn ( ( ~P A ^ko ~P A ) \|`t ( Base ` G ) ) ) = ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) )
170	166 169	eleqtrd	\|- ( A e. V -> ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) )
171		eqid	\|- ( TopOpen ` G ) = ( TopOpen ` G )
172	171 142	istgp	\|- ( G e. TopGrp <-> ( G e. Grp /\ G e. TopMnd /\ ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) ) )
173	2 9 170 172	syl3anbrc	\|- ( A e. V -> G e. TopGrp )

Metamath Proof Explorer

Theorem symgtgp

Proof