Metamath Proof Explorer

Theorem 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 syl5ibr 
 |-  ( 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 ffvelrnda 
 |-  ( ( ( 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 ffvelrnd 
 |-  ( ( ( 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 )