Step |
Hyp |
Ref |
Expression |
1 |
|
prdstgpd.y |
|- Y = ( S Xs_ R ) |
2 |
|
prdstgpd.i |
|- ( ph -> I e. W ) |
3 |
|
prdstgpd.s |
|- ( ph -> S e. V ) |
4 |
|
prdstgpd.r |
|- ( ph -> R : I --> TopGrp ) |
5 |
|
tgpgrp |
|- ( x e. TopGrp -> x e. Grp ) |
6 |
5
|
ssriv |
|- TopGrp C_ Grp |
7 |
|
fss |
|- ( ( R : I --> TopGrp /\ TopGrp C_ Grp ) -> R : I --> Grp ) |
8 |
4 6 7
|
sylancl |
|- ( ph -> R : I --> Grp ) |
9 |
1 2 3 8
|
prdsgrpd |
|- ( ph -> Y e. Grp ) |
10 |
|
tgptmd |
|- ( x e. TopGrp -> x e. TopMnd ) |
11 |
10
|
ssriv |
|- TopGrp C_ TopMnd |
12 |
|
fss |
|- ( ( R : I --> TopGrp /\ TopGrp C_ TopMnd ) -> R : I --> TopMnd ) |
13 |
4 11 12
|
sylancl |
|- ( ph -> R : I --> TopMnd ) |
14 |
1 2 3 13
|
prdstmdd |
|- ( ph -> Y e. TopMnd ) |
15 |
|
eqid |
|- ( Xt_ ` ( TopOpen o. R ) ) = ( Xt_ ` ( TopOpen o. R ) ) |
16 |
|
eqid |
|- ( TopOpen ` Y ) = ( TopOpen ` Y ) |
17 |
|
eqid |
|- ( Base ` Y ) = ( Base ` Y ) |
18 |
16 17
|
tmdtopon |
|- ( Y e. TopMnd -> ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) ) |
19 |
14 18
|
syl |
|- ( ph -> ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) ) |
20 |
|
topnfn |
|- TopOpen Fn _V |
21 |
4
|
ffnd |
|- ( ph -> R Fn I ) |
22 |
|
dffn2 |
|- ( R Fn I <-> R : I --> _V ) |
23 |
21 22
|
sylib |
|- ( ph -> R : I --> _V ) |
24 |
|
fnfco |
|- ( ( TopOpen Fn _V /\ R : I --> _V ) -> ( TopOpen o. R ) Fn I ) |
25 |
20 23 24
|
sylancr |
|- ( ph -> ( TopOpen o. R ) Fn I ) |
26 |
|
fvco3 |
|- ( ( R : I --> TopGrp /\ y e. I ) -> ( ( TopOpen o. R ) ` y ) = ( TopOpen ` ( R ` y ) ) ) |
27 |
4 26
|
sylan |
|- ( ( ph /\ y e. I ) -> ( ( TopOpen o. R ) ` y ) = ( TopOpen ` ( R ` y ) ) ) |
28 |
4
|
ffvelrnda |
|- ( ( ph /\ y e. I ) -> ( R ` y ) e. TopGrp ) |
29 |
|
eqid |
|- ( TopOpen ` ( R ` y ) ) = ( TopOpen ` ( R ` y ) ) |
30 |
|
eqid |
|- ( Base ` ( R ` y ) ) = ( Base ` ( R ` y ) ) |
31 |
29 30
|
tgptopon |
|- ( ( R ` y ) e. TopGrp -> ( TopOpen ` ( R ` y ) ) e. ( TopOn ` ( Base ` ( R ` y ) ) ) ) |
32 |
|
topontop |
|- ( ( TopOpen ` ( R ` y ) ) e. ( TopOn ` ( Base ` ( R ` y ) ) ) -> ( TopOpen ` ( R ` y ) ) e. Top ) |
33 |
28 31 32
|
3syl |
|- ( ( ph /\ y e. I ) -> ( TopOpen ` ( R ` y ) ) e. Top ) |
34 |
27 33
|
eqeltrd |
|- ( ( ph /\ y e. I ) -> ( ( TopOpen o. R ) ` y ) e. Top ) |
35 |
34
|
ralrimiva |
|- ( ph -> A. y e. I ( ( TopOpen o. R ) ` y ) e. Top ) |
36 |
|
ffnfv |
|- ( ( TopOpen o. R ) : I --> Top <-> ( ( TopOpen o. R ) Fn I /\ A. y e. I ( ( TopOpen o. R ) ` y ) e. Top ) ) |
37 |
25 35 36
|
sylanbrc |
|- ( ph -> ( TopOpen o. R ) : I --> Top ) |
38 |
19
|
adantr |
|- ( ( ph /\ y e. I ) -> ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) ) |
39 |
1 3 2 21 16
|
prdstopn |
|- ( ph -> ( TopOpen ` Y ) = ( Xt_ ` ( TopOpen o. R ) ) ) |
40 |
39
|
adantr |
|- ( ( ph /\ y e. I ) -> ( TopOpen ` Y ) = ( Xt_ ` ( TopOpen o. R ) ) ) |
41 |
40
|
eqcomd |
|- ( ( ph /\ y e. I ) -> ( Xt_ ` ( TopOpen o. R ) ) = ( TopOpen ` Y ) ) |
42 |
41 38
|
eqeltrd |
|- ( ( ph /\ y e. I ) -> ( Xt_ ` ( TopOpen o. R ) ) e. ( TopOn ` ( Base ` Y ) ) ) |
43 |
|
toponuni |
|- ( ( Xt_ ` ( TopOpen o. R ) ) e. ( TopOn ` ( Base ` Y ) ) -> ( Base ` Y ) = U. ( Xt_ ` ( TopOpen o. R ) ) ) |
44 |
|
mpteq1 |
|- ( ( Base ` Y ) = U. ( Xt_ ` ( TopOpen o. R ) ) -> ( x e. ( Base ` Y ) |-> ( x ` y ) ) = ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` y ) ) ) |
45 |
42 43 44
|
3syl |
|- ( ( ph /\ y e. I ) -> ( x e. ( Base ` Y ) |-> ( x ` y ) ) = ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` y ) ) ) |
46 |
2
|
adantr |
|- ( ( ph /\ y e. I ) -> I e. W ) |
47 |
37
|
adantr |
|- ( ( ph /\ y e. I ) -> ( TopOpen o. R ) : I --> Top ) |
48 |
|
simpr |
|- ( ( ph /\ y e. I ) -> y e. I ) |
49 |
|
eqid |
|- U. ( Xt_ ` ( TopOpen o. R ) ) = U. ( Xt_ ` ( TopOpen o. R ) ) |
50 |
49 15
|
ptpjcn |
|- ( ( I e. W /\ ( TopOpen o. R ) : I --> Top /\ y e. I ) -> ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` y ) ) e. ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` y ) ) ) |
51 |
46 47 48 50
|
syl3anc |
|- ( ( ph /\ y e. I ) -> ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` y ) ) e. ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` y ) ) ) |
52 |
45 51
|
eqeltrd |
|- ( ( ph /\ y e. I ) -> ( x e. ( Base ` Y ) |-> ( x ` y ) ) e. ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` y ) ) ) |
53 |
41 27
|
oveq12d |
|- ( ( ph /\ y e. I ) -> ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` y ) ) = ( ( TopOpen ` Y ) Cn ( TopOpen ` ( R ` y ) ) ) ) |
54 |
52 53
|
eleqtrd |
|- ( ( ph /\ y e. I ) -> ( x e. ( Base ` Y ) |-> ( x ` y ) ) e. ( ( TopOpen ` Y ) Cn ( TopOpen ` ( R ` y ) ) ) ) |
55 |
|
eqid |
|- ( invg ` ( R ` y ) ) = ( invg ` ( R ` y ) ) |
56 |
29 55
|
tgpinv |
|- ( ( R ` y ) e. TopGrp -> ( invg ` ( R ` y ) ) e. ( ( TopOpen ` ( R ` y ) ) Cn ( TopOpen ` ( R ` y ) ) ) ) |
57 |
28 56
|
syl |
|- ( ( ph /\ y e. I ) -> ( invg ` ( R ` y ) ) e. ( ( TopOpen ` ( R ` y ) ) Cn ( TopOpen ` ( R ` y ) ) ) ) |
58 |
38 54 57
|
cnmpt11f |
|- ( ( ph /\ y e. I ) -> ( x e. ( Base ` Y ) |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) e. ( ( TopOpen ` Y ) Cn ( TopOpen ` ( R ` y ) ) ) ) |
59 |
27
|
oveq2d |
|- ( ( ph /\ y e. I ) -> ( ( TopOpen ` Y ) Cn ( ( TopOpen o. R ) ` y ) ) = ( ( TopOpen ` Y ) Cn ( TopOpen ` ( R ` y ) ) ) ) |
60 |
58 59
|
eleqtrrd |
|- ( ( ph /\ y e. I ) -> ( x e. ( Base ` Y ) |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) e. ( ( TopOpen ` Y ) Cn ( ( TopOpen o. R ) ` y ) ) ) |
61 |
15 19 2 37 60
|
ptcn |
|- ( ph -> ( x e. ( Base ` Y ) |-> ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) ) e. ( ( TopOpen ` Y ) Cn ( Xt_ ` ( TopOpen o. R ) ) ) ) |
62 |
|
eqid |
|- ( invg ` Y ) = ( invg ` Y ) |
63 |
17 62
|
grpinvf |
|- ( Y e. Grp -> ( invg ` Y ) : ( Base ` Y ) --> ( Base ` Y ) ) |
64 |
9 63
|
syl |
|- ( ph -> ( invg ` Y ) : ( Base ` Y ) --> ( Base ` Y ) ) |
65 |
64
|
feqmptd |
|- ( ph -> ( invg ` Y ) = ( x e. ( Base ` Y ) |-> ( ( invg ` Y ) ` x ) ) ) |
66 |
2
|
adantr |
|- ( ( ph /\ x e. ( Base ` Y ) ) -> I e. W ) |
67 |
3
|
adantr |
|- ( ( ph /\ x e. ( Base ` Y ) ) -> S e. V ) |
68 |
8
|
adantr |
|- ( ( ph /\ x e. ( Base ` Y ) ) -> R : I --> Grp ) |
69 |
|
simpr |
|- ( ( ph /\ x e. ( Base ` Y ) ) -> x e. ( Base ` Y ) ) |
70 |
1 66 67 68 17 62 69
|
prdsinvgd |
|- ( ( ph /\ x e. ( Base ` Y ) ) -> ( ( invg ` Y ) ` x ) = ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) ) |
71 |
70
|
mpteq2dva |
|- ( ph -> ( x e. ( Base ` Y ) |-> ( ( invg ` Y ) ` x ) ) = ( x e. ( Base ` Y ) |-> ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) ) ) |
72 |
65 71
|
eqtrd |
|- ( ph -> ( invg ` Y ) = ( x e. ( Base ` Y ) |-> ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) ) ) |
73 |
39
|
oveq2d |
|- ( ph -> ( ( TopOpen ` Y ) Cn ( TopOpen ` Y ) ) = ( ( TopOpen ` Y ) Cn ( Xt_ ` ( TopOpen o. R ) ) ) ) |
74 |
61 72 73
|
3eltr4d |
|- ( ph -> ( invg ` Y ) e. ( ( TopOpen ` Y ) Cn ( TopOpen ` Y ) ) ) |
75 |
16 62
|
istgp |
|- ( Y e. TopGrp <-> ( Y e. Grp /\ Y e. TopMnd /\ ( invg ` Y ) e. ( ( TopOpen ` Y ) Cn ( TopOpen ` Y ) ) ) ) |
76 |
9 14 74 75
|
syl3anbrc |
|- ( ph -> Y e. TopGrp ) |