Step |
Hyp |
Ref |
Expression |
1 |
|
snclseqg.x |
|- X = ( Base ` G ) |
2 |
|
snclseqg.j |
|- J = ( TopOpen ` G ) |
3 |
|
snclseqg.z |
|- .0. = ( 0g ` G ) |
4 |
|
snclseqg.r |
|- .~ = ( G ~QG S ) |
5 |
|
snclseqg.s |
|- S = ( ( cls ` J ) ` { .0. } ) |
6 |
5
|
imaeq2i |
|- ( ( x e. X |-> ( A ( +g ` G ) x ) ) " S ) = ( ( x e. X |-> ( A ( +g ` G ) x ) ) " ( ( cls ` J ) ` { .0. } ) ) |
7 |
|
tgpgrp |
|- ( G e. TopGrp -> G e. Grp ) |
8 |
7
|
adantr |
|- ( ( G e. TopGrp /\ A e. X ) -> G e. Grp ) |
9 |
2 1
|
tgptopon |
|- ( G e. TopGrp -> J e. ( TopOn ` X ) ) |
10 |
9
|
adantr |
|- ( ( G e. TopGrp /\ A e. X ) -> J e. ( TopOn ` X ) ) |
11 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
12 |
10 11
|
syl |
|- ( ( G e. TopGrp /\ A e. X ) -> J e. Top ) |
13 |
1 3
|
grpidcl |
|- ( G e. Grp -> .0. e. X ) |
14 |
8 13
|
syl |
|- ( ( G e. TopGrp /\ A e. X ) -> .0. e. X ) |
15 |
14
|
snssd |
|- ( ( G e. TopGrp /\ A e. X ) -> { .0. } C_ X ) |
16 |
|
toponuni |
|- ( J e. ( TopOn ` X ) -> X = U. J ) |
17 |
10 16
|
syl |
|- ( ( G e. TopGrp /\ A e. X ) -> X = U. J ) |
18 |
15 17
|
sseqtrd |
|- ( ( G e. TopGrp /\ A e. X ) -> { .0. } C_ U. J ) |
19 |
|
eqid |
|- U. J = U. J |
20 |
19
|
clsss3 |
|- ( ( J e. Top /\ { .0. } C_ U. J ) -> ( ( cls ` J ) ` { .0. } ) C_ U. J ) |
21 |
12 18 20
|
syl2anc |
|- ( ( G e. TopGrp /\ A e. X ) -> ( ( cls ` J ) ` { .0. } ) C_ U. J ) |
22 |
21 17
|
sseqtrrd |
|- ( ( G e. TopGrp /\ A e. X ) -> ( ( cls ` J ) ` { .0. } ) C_ X ) |
23 |
5 22
|
eqsstrid |
|- ( ( G e. TopGrp /\ A e. X ) -> S C_ X ) |
24 |
|
simpr |
|- ( ( G e. TopGrp /\ A e. X ) -> A e. X ) |
25 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
26 |
1 4 25
|
eqglact |
|- ( ( G e. Grp /\ S C_ X /\ A e. X ) -> [ A ] .~ = ( ( x e. X |-> ( A ( +g ` G ) x ) ) " S ) ) |
27 |
8 23 24 26
|
syl3anc |
|- ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ = ( ( x e. X |-> ( A ( +g ` G ) x ) ) " S ) ) |
28 |
|
eqid |
|- ( x e. X |-> ( A ( +g ` G ) x ) ) = ( x e. X |-> ( A ( +g ` G ) x ) ) |
29 |
28 1 25 2
|
tgplacthmeo |
|- ( ( G e. TopGrp /\ A e. X ) -> ( x e. X |-> ( A ( +g ` G ) x ) ) e. ( J Homeo J ) ) |
30 |
19
|
hmeocls |
|- ( ( ( x e. X |-> ( A ( +g ` G ) x ) ) e. ( J Homeo J ) /\ { .0. } C_ U. J ) -> ( ( cls ` J ) ` ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) ) = ( ( x e. X |-> ( A ( +g ` G ) x ) ) " ( ( cls ` J ) ` { .0. } ) ) ) |
31 |
29 18 30
|
syl2anc |
|- ( ( G e. TopGrp /\ A e. X ) -> ( ( cls ` J ) ` ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) ) = ( ( x e. X |-> ( A ( +g ` G ) x ) ) " ( ( cls ` J ) ` { .0. } ) ) ) |
32 |
6 27 31
|
3eqtr4a |
|- ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ = ( ( cls ` J ) ` ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) ) ) |
33 |
|
df-ima |
|- ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) = ran ( ( x e. X |-> ( A ( +g ` G ) x ) ) |` { .0. } ) |
34 |
15
|
resmptd |
|- ( ( G e. TopGrp /\ A e. X ) -> ( ( x e. X |-> ( A ( +g ` G ) x ) ) |` { .0. } ) = ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) ) |
35 |
34
|
rneqd |
|- ( ( G e. TopGrp /\ A e. X ) -> ran ( ( x e. X |-> ( A ( +g ` G ) x ) ) |` { .0. } ) = ran ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) ) |
36 |
33 35
|
syl5eq |
|- ( ( G e. TopGrp /\ A e. X ) -> ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) = ran ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) ) |
37 |
3
|
fvexi |
|- .0. e. _V |
38 |
|
oveq2 |
|- ( x = .0. -> ( A ( +g ` G ) x ) = ( A ( +g ` G ) .0. ) ) |
39 |
38
|
eqeq2d |
|- ( x = .0. -> ( y = ( A ( +g ` G ) x ) <-> y = ( A ( +g ` G ) .0. ) ) ) |
40 |
37 39
|
rexsn |
|- ( E. x e. { .0. } y = ( A ( +g ` G ) x ) <-> y = ( A ( +g ` G ) .0. ) ) |
41 |
1 25 3
|
grprid |
|- ( ( G e. Grp /\ A e. X ) -> ( A ( +g ` G ) .0. ) = A ) |
42 |
7 41
|
sylan |
|- ( ( G e. TopGrp /\ A e. X ) -> ( A ( +g ` G ) .0. ) = A ) |
43 |
42
|
eqeq2d |
|- ( ( G e. TopGrp /\ A e. X ) -> ( y = ( A ( +g ` G ) .0. ) <-> y = A ) ) |
44 |
40 43
|
syl5bb |
|- ( ( G e. TopGrp /\ A e. X ) -> ( E. x e. { .0. } y = ( A ( +g ` G ) x ) <-> y = A ) ) |
45 |
44
|
abbidv |
|- ( ( G e. TopGrp /\ A e. X ) -> { y | E. x e. { .0. } y = ( A ( +g ` G ) x ) } = { y | y = A } ) |
46 |
|
eqid |
|- ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) = ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) |
47 |
46
|
rnmpt |
|- ran ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) = { y | E. x e. { .0. } y = ( A ( +g ` G ) x ) } |
48 |
|
df-sn |
|- { A } = { y | y = A } |
49 |
45 47 48
|
3eqtr4g |
|- ( ( G e. TopGrp /\ A e. X ) -> ran ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) = { A } ) |
50 |
36 49
|
eqtrd |
|- ( ( G e. TopGrp /\ A e. X ) -> ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) = { A } ) |
51 |
50
|
fveq2d |
|- ( ( G e. TopGrp /\ A e. X ) -> ( ( cls ` J ) ` ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) ) = ( ( cls ` J ) ` { A } ) ) |
52 |
32 51
|
eqtrd |
|- ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ = ( ( cls ` J ) ` { A } ) ) |