Step | Hyp | Ref
| Expression |
1 | | symgtgp.g |
. . 3
β’ πΊ = (SymGrpβπ΄) |
2 | 1 | symggrp 19190 |
. 2
β’ (π΄ β π β πΊ β Grp) |
3 | | eqid 2733 |
. . . 4
β’
(EndoFMndβπ΄) =
(EndoFMndβπ΄) |
4 | 3 | efmndtmd 23475 |
. . 3
β’ (π΄ β π β (EndoFMndβπ΄) β TopMnd) |
5 | | eqid 2733 |
. . . 4
β’
(BaseβπΊ) =
(BaseβπΊ) |
6 | 3, 1, 5 | symgsubmefmnd 19188 |
. . 3
β’ (π΄ β π β (BaseβπΊ) β (SubMndβ(EndoFMndβπ΄))) |
7 | 1, 5, 3 | symgressbas 19171 |
. . . 4
β’ πΊ = ((EndoFMndβπ΄) βΎs
(BaseβπΊ)) |
8 | 7 | submtmd 23478 |
. . 3
β’
(((EndoFMndβπ΄)
β TopMnd β§ (BaseβπΊ) β (SubMndβ(EndoFMndβπ΄))) β πΊ β TopMnd) |
9 | 4, 6, 8 | syl2anc 585 |
. 2
β’ (π΄ β π β πΊ β TopMnd) |
10 | | eqid 2733 |
. . . . . 6
β’
(βtβ(π΄ Γ {π« π΄})) = (βtβ(π΄ Γ {π« π΄})) |
11 | 1, 5 | symgtopn 19196 |
. . . . . . 7
β’ (π΄ β π β ((βtβ(π΄ Γ {π« π΄})) βΎt
(BaseβπΊ)) =
(TopOpenβπΊ)) |
12 | | distopon 22370 |
. . . . . . . . 9
β’ (π΄ β π β π« π΄ β (TopOnβπ΄)) |
13 | 10 | pttoponconst 22971 |
. . . . . . . . 9
β’ ((π΄ β π β§ π« π΄ β (TopOnβπ΄)) β (βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄))) |
14 | 12, 13 | mpdan 686 |
. . . . . . . 8
β’ (π΄ β π β (βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄))) |
15 | 1, 5 | elsymgbas 19163 |
. . . . . . . . . 10
β’ (π΄ β π β (π₯ β (BaseβπΊ) β π₯:π΄β1-1-ontoβπ΄)) |
16 | | f1of 6788 |
. . . . . . . . . . 11
β’ (π₯:π΄β1-1-ontoβπ΄ β π₯:π΄βΆπ΄) |
17 | | elmapg 8784 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ π΄ β π) β (π₯ β (π΄ βm π΄) β π₯:π΄βΆπ΄)) |
18 | 17 | anidms 568 |
. . . . . . . . . . 11
β’ (π΄ β π β (π₯ β (π΄ βm π΄) β π₯:π΄βΆπ΄)) |
19 | 16, 18 | syl5ibr 246 |
. . . . . . . . . 10
β’ (π΄ β π β (π₯:π΄β1-1-ontoβπ΄ β π₯ β (π΄ βm π΄))) |
20 | 15, 19 | sylbid 239 |
. . . . . . . . 9
β’ (π΄ β π β (π₯ β (BaseβπΊ) β π₯ β (π΄ βm π΄))) |
21 | 20 | ssrdv 3954 |
. . . . . . . 8
β’ (π΄ β π β (BaseβπΊ) β (π΄ βm π΄)) |
22 | | resttopon 22535 |
. . . . . . . 8
β’
(((βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄)) β§ (BaseβπΊ) β (π΄ βm π΄)) β ((βtβ(π΄ Γ {π« π΄})) βΎt
(BaseβπΊ)) β
(TopOnβ(BaseβπΊ))) |
23 | 14, 21, 22 | syl2anc 585 |
. . . . . . 7
β’ (π΄ β π β ((βtβ(π΄ Γ {π« π΄})) βΎt
(BaseβπΊ)) β
(TopOnβ(BaseβπΊ))) |
24 | 11, 23 | eqeltrrd 2835 |
. . . . . 6
β’ (π΄ β π β (TopOpenβπΊ) β (TopOnβ(BaseβπΊ))) |
25 | | id 22 |
. . . . . 6
β’ (π΄ β π β π΄ β π) |
26 | | distop 22368 |
. . . . . . 7
β’ (π΄ β π β π« π΄ β Top) |
27 | | fconst6g 6735 |
. . . . . . 7
β’
(π« π΄ β
Top β (π΄ Γ
{π« π΄}):π΄βΆTop) |
28 | 26, 27 | syl 17 |
. . . . . 6
β’ (π΄ β π β (π΄ Γ {π« π΄}):π΄βΆTop) |
29 | 15 | biimpa 478 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ π₯ β (BaseβπΊ)) β π₯:π΄β1-1-ontoβπ΄) |
30 | | f1ocnv 6800 |
. . . . . . . . . . . 12
β’ (π₯:π΄β1-1-ontoβπ΄ β β‘π₯:π΄β1-1-ontoβπ΄) |
31 | | f1of 6788 |
. . . . . . . . . . . 12
β’ (β‘π₯:π΄β1-1-ontoβπ΄ β β‘π₯:π΄βΆπ΄) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ π₯ β (BaseβπΊ)) β β‘π₯:π΄βΆπ΄) |
33 | 32 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π₯ β (BaseβπΊ)) β§ π¦ β π΄) β (β‘π₯βπ¦) β π΄) |
34 | 33 | an32s 651 |
. . . . . . . . 9
β’ (((π΄ β π β§ π¦ β π΄) β§ π₯ β (BaseβπΊ)) β (β‘π₯βπ¦) β π΄) |
35 | 34 | fmpttd 7067 |
. . . . . . . 8
β’ ((π΄ β π β§ π¦ β π΄) β (π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)):(BaseβπΊ)βΆπ΄) |
36 | 35 | adantr 482 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)):(BaseβπΊ)βΆπ΄) |
37 | | cnveq 5833 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β β‘π₯ = β‘π) |
38 | 37 | fveq1d 6848 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (β‘π₯βπ¦) = (β‘πβπ¦)) |
39 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) = (π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) |
40 | | fvex 6859 |
. . . . . . . . . . . . . . 15
β’ (β‘πβπ¦) β V |
41 | 38, 39, 40 | fvmpt 6952 |
. . . . . . . . . . . . . 14
β’ (π β (BaseβπΊ) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦))βπ) = (β‘πβπ¦)) |
42 | 41 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ π‘ β π« π΄) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦))βπ) = (β‘πβπ¦)) |
43 | 42 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ π‘ β π« π΄) β (((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦))βπ) β π‘ β (β‘πβπ¦) β π‘)) |
44 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β (BaseβπΊ) β¦ (π’β(β‘πβπ¦))) = (π’ β (BaseβπΊ) β¦ (π’β(β‘πβπ¦))) |
45 | 44 | mptiniseg 6195 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β V β (β‘(π’ β (BaseβπΊ) β¦ (π’β(β‘πβπ¦))) β {π¦}) = {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦}) |
46 | 45 | elv 3453 |
. . . . . . . . . . . . . . . 16
β’ (β‘(π’ β (BaseβπΊ) β¦ (π’β(β‘πβπ¦))) β {π¦}) = {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} |
47 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
((βtβ(π΄ Γ {π« π΄})) βΎt (BaseβπΊ)) =
((βtβ(π΄ Γ {π« π΄})) βΎt (BaseβπΊ)) |
48 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄))) |
49 | 21 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (BaseβπΊ) β (π΄ βm π΄)) |
50 | | toponuni 22286 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((βtβ(π΄ Γ {π« π΄})) β (TopOnβ(π΄ βm π΄)) β (π΄ βm π΄) = βͺ
(βtβ(π΄ Γ {π« π΄}))) |
51 | | mpteq1 5202 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ βm π΄) = βͺ
(βtβ(π΄ Γ {π« π΄})) β (π’ β (π΄ βm π΄) β¦ (π’β(β‘πβπ¦))) = (π’ β βͺ
(βtβ(π΄ Γ {π« π΄})) β¦ (π’β(β‘πβπ¦)))) |
52 | 48, 50, 51 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (π’ β (π΄ βm π΄) β¦ (π’β(β‘πβπ¦))) = (π’ β βͺ
(βtβ(π΄ Γ {π« π΄})) β¦ (π’β(β‘πβπ¦)))) |
53 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β π΄ β π) |
54 | 28 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (π΄ Γ {π« π΄}):π΄βΆTop) |
55 | 1, 5 | elsymgbas 19163 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π΄ β π β (π β (BaseβπΊ) β π:π΄β1-1-ontoβπ΄)) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π΄ β π β§ π¦ β π΄) β (π β (BaseβπΊ) β π:π΄β1-1-ontoβπ΄)) |
57 | 56 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β π:π΄β1-1-ontoβπ΄) |
58 | | f1ocnv 6800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π:π΄β1-1-ontoβπ΄ β β‘π:π΄β1-1-ontoβπ΄) |
59 | | f1of 6788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (β‘π:π΄β1-1-ontoβπ΄ β β‘π:π΄βΆπ΄) |
60 | 57, 58, 59 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β β‘π:π΄βΆπ΄) |
61 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β π¦ β π΄) |
62 | 60, 61 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (β‘πβπ¦) β π΄) |
63 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ βͺ (βtβ(π΄ Γ {π« π΄})) = βͺ
(βtβ(π΄ Γ {π« π΄})) |
64 | 63, 10 | ptpjcn 22985 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β π β§ (π΄ Γ {π« π΄}):π΄βΆTop β§ (β‘πβπ¦) β π΄) β (π’ β βͺ
(βtβ(π΄ Γ {π« π΄})) β¦ (π’β(β‘πβπ¦))) β ((βtβ(π΄ Γ {π« π΄})) Cn ((π΄ Γ {π« π΄})β(β‘πβπ¦)))) |
65 | 53, 54, 62, 64 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (π’ β βͺ
(βtβ(π΄ Γ {π« π΄})) β¦ (π’β(β‘πβπ¦))) β ((βtβ(π΄ Γ {π« π΄})) Cn ((π΄ Γ {π« π΄})β(β‘πβπ¦)))) |
66 | 26 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β π« π΄ β Top) |
67 | | fvconst2g 7155 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((π« π΄ β
Top β§ (β‘πβπ¦) β π΄) β ((π΄ Γ {π« π΄})β(β‘πβπ¦)) = π« π΄) |
68 | 66, 62, 67 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β ((π΄ Γ {π« π΄})β(β‘πβπ¦)) = π« π΄) |
69 | 68 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β ((βtβ(π΄ Γ {π« π΄})) Cn ((π΄ Γ {π« π΄})β(β‘πβπ¦))) = ((βtβ(π΄ Γ {π« π΄})) Cn π« π΄)) |
70 | 65, 69 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (π’ β βͺ
(βtβ(π΄ Γ {π« π΄})) β¦ (π’β(β‘πβπ¦))) β ((βtβ(π΄ Γ {π« π΄})) Cn π« π΄)) |
71 | 52, 70 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (π’ β (π΄ βm π΄) β¦ (π’β(β‘πβπ¦))) β ((βtβ(π΄ Γ {π« π΄})) Cn π« π΄)) |
72 | 47, 48, 49, 71 | cnmpt1res 23050 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (π’ β (BaseβπΊ) β¦ (π’β(β‘πβπ¦))) β (((βtβ(π΄ Γ {π« π΄})) βΎt
(BaseβπΊ)) Cn
π« π΄)) |
73 | 11 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β π β (((βtβ(π΄ Γ {π« π΄})) βΎt
(BaseβπΊ)) Cn
π« π΄) =
((TopOpenβπΊ) Cn
π« π΄)) |
74 | 73 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (((βtβ(π΄ Γ {π« π΄})) βΎt
(BaseβπΊ)) Cn
π« π΄) =
((TopOpenβπΊ) Cn
π« π΄)) |
75 | 72, 74 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (π’ β (BaseβπΊ) β¦ (π’β(β‘πβπ¦))) β ((TopOpenβπΊ) Cn π« π΄)) |
76 | | snelpwi 5404 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β π΄ β {π¦} β π« π΄) |
77 | 76 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β {π¦} β π« π΄) |
78 | | cnima 22639 |
. . . . . . . . . . . . . . . . 17
β’ (((π’ β (BaseβπΊ) β¦ (π’β(β‘πβπ¦))) β ((TopOpenβπΊ) Cn π« π΄) β§ {π¦} β π« π΄) β (β‘(π’ β (BaseβπΊ) β¦ (π’β(β‘πβπ¦))) β {π¦}) β (TopOpenβπΊ)) |
79 | 75, 77, 78 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (β‘(π’ β (BaseβπΊ) β¦ (π’β(β‘πβπ¦))) β {π¦}) β (TopOpenβπΊ)) |
80 | 46, 79 | eqeltrrid 2839 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (TopOpenβπΊ)) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (TopOpenβπΊ)) |
82 | | fveq1 6845 |
. . . . . . . . . . . . . . . 16
β’ (π’ = π β (π’β(β‘πβπ¦)) = (πβ(β‘πβπ¦))) |
83 | 82 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
β’ (π’ = π β ((π’β(β‘πβπ¦)) = π¦ β (πβ(β‘πβπ¦)) = π¦)) |
84 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β π β (BaseβπΊ)) |
85 | 57 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β π:π΄β1-1-ontoβπ΄) |
86 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β π¦ β π΄) |
87 | | f1ocnvfv2 7227 |
. . . . . . . . . . . . . . . 16
β’ ((π:π΄β1-1-ontoβπ΄ β§ π¦ β π΄) β (πβ(β‘πβπ¦)) = π¦) |
88 | 85, 86, 87 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β (πβ(β‘πβπ¦)) = π¦) |
89 | 83, 84, 88 | elrabd 3651 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β π β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦}) |
90 | | ssrab2 4041 |
. . . . . . . . . . . . . . . . . 18
β’ {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (BaseβπΊ) |
91 | 90 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (BaseβπΊ)) |
92 | 15 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β (π₯ β (BaseβπΊ) β π₯:π΄β1-1-ontoβπ΄)) |
93 | 92 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β§ π₯ β (BaseβπΊ)) β π₯:π΄β1-1-ontoβπ΄) |
94 | 62 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β§ π₯ β (BaseβπΊ)) β (β‘πβπ¦) β π΄) |
95 | | f1ocnvfv 7228 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯:π΄β1-1-ontoβπ΄ β§ (β‘πβπ¦) β π΄) β ((π₯β(β‘πβπ¦)) = π¦ β (β‘π₯βπ¦) = (β‘πβπ¦))) |
96 | 93, 94, 95 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β§ π₯ β (BaseβπΊ)) β ((π₯β(β‘πβπ¦)) = π¦ β (β‘π₯βπ¦) = (β‘πβπ¦))) |
97 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β§ π₯ β (BaseβπΊ)) β (β‘πβπ¦) β π‘) |
98 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β‘π₯βπ¦) = (β‘πβπ¦) β ((β‘π₯βπ¦) β π‘ β (β‘πβπ¦) β π‘)) |
99 | 97, 98 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β§ π₯ β (BaseβπΊ)) β ((β‘π₯βπ¦) = (β‘πβπ¦) β (β‘π₯βπ¦) β π‘)) |
100 | 96, 99 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β§ π₯ β (BaseβπΊ)) β ((π₯β(β‘πβπ¦)) = π¦ β (β‘π₯βπ¦) β π‘)) |
101 | 100 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β βπ₯ β (BaseβπΊ)((π₯β(β‘πβπ¦)) = π¦ β (β‘π₯βπ¦) β π‘)) |
102 | | fveq1 6845 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π’ = π₯ β (π’β(β‘πβπ¦)) = (π₯β(β‘πβπ¦))) |
103 | 102 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ = π₯ β ((π’β(β‘πβπ¦)) = π¦ β (π₯β(β‘πβπ¦)) = π¦)) |
104 | 103 | ralrab 3655 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ₯ β
{π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} (β‘π₯βπ¦) β π‘ β βπ₯ β (BaseβπΊ)((π₯β(β‘πβπ¦)) = π¦ β (β‘π₯βπ¦) β π‘)) |
105 | 101, 104 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β βπ₯ β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} (β‘π₯βπ¦) β π‘) |
106 | | ssrab 4034 |
. . . . . . . . . . . . . . . . 17
β’ ({π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β {π₯ β (BaseβπΊ) β£ (β‘π₯βπ¦) β π‘} β ({π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (BaseβπΊ) β§ βπ₯ β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} (β‘π₯βπ¦) β π‘)) |
107 | 91, 105, 106 | sylanbrc 584 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β {π₯ β (BaseβπΊ) β£ (β‘π₯βπ¦) β π‘}) |
108 | 39 | mptpreima 6194 |
. . . . . . . . . . . . . . . 16
β’ (β‘(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π‘) = {π₯ β (BaseβπΊ) β£ (β‘π₯βπ¦) β π‘} |
109 | 107, 108 | sseqtrrdi 3999 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (β‘(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π‘)) |
110 | | funmpt 6543 |
. . . . . . . . . . . . . . . 16
β’ Fun
(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) |
111 | | fvex 6859 |
. . . . . . . . . . . . . . . . . 18
β’ (β‘π₯βπ¦) β V |
112 | 111, 39 | dmmpti 6649 |
. . . . . . . . . . . . . . . . 17
β’ dom
(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) = (BaseβπΊ) |
113 | 91, 112 | sseqtrrdi 3999 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β dom (π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦))) |
114 | | funimass3 7008 |
. . . . . . . . . . . . . . . 16
β’ ((Fun
(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β§ {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β dom (π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦))) β (((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦}) β π‘ β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (β‘(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π‘))) |
115 | 110, 113,
114 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β (((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦}) β π‘ β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (β‘(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π‘))) |
116 | 109, 115 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦}) β π‘) |
117 | | eleq2 2823 |
. . . . . . . . . . . . . . . 16
β’ (π£ = {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (π β π£ β π β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦})) |
118 | | imaeq2 6013 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π£) = ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦})) |
119 | 118 | sseq1d 3979 |
. . . . . . . . . . . . . . . 16
β’ (π£ = {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π£) β π‘ β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦}) β π‘)) |
120 | 117, 119 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π£ = {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β ((π β π£ β§ ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π£) β π‘) β (π β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β§ ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦}) β π‘))) |
121 | 120 | rspcev 3583 |
. . . . . . . . . . . . . 14
β’ (({π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β (TopOpenβπΊ) β§ (π β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦} β§ ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β {π’ β (BaseβπΊ) β£ (π’β(β‘πβπ¦)) = π¦}) β π‘)) β βπ£ β (TopOpenβπΊ)(π β π£ β§ ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π£) β π‘)) |
122 | 81, 89, 116, 121 | syl12anc 836 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ (π‘ β π« π΄ β§ (β‘πβπ¦) β π‘)) β βπ£ β (TopOpenβπΊ)(π β π£ β§ ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π£) β π‘)) |
123 | 122 | expr 458 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ π‘ β π« π΄) β ((β‘πβπ¦) β π‘ β βπ£ β (TopOpenβπΊ)(π β π£ β§ ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π£) β π‘))) |
124 | 43, 123 | sylbid 239 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β§ π‘ β π« π΄) β (((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦))βπ) β π‘ β βπ£ β (TopOpenβπΊ)(π β π£ β§ ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π£) β π‘))) |
125 | 124 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β βπ‘ β π« π΄(((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦))βπ) β π‘ β βπ£ β (TopOpenβπΊ)(π β π£ β§ ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π£) β π‘))) |
126 | 24 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (TopOpenβπΊ) β (TopOnβ(BaseβπΊ))) |
127 | 12 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β π« π΄ β (TopOnβπ΄)) |
128 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β π β (BaseβπΊ)) |
129 | | iscnp 22611 |
. . . . . . . . . . 11
β’
(((TopOpenβπΊ)
β (TopOnβ(BaseβπΊ)) β§ π« π΄ β (TopOnβπ΄) β§ π β (BaseβπΊ)) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β (((TopOpenβπΊ) CnP π« π΄)βπ) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)):(BaseβπΊ)βΆπ΄ β§ βπ‘ β π« π΄(((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦))βπ) β π‘ β βπ£ β (TopOpenβπΊ)(π β π£ β§ ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π£) β π‘))))) |
130 | 126, 127,
128, 129 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β (((TopOpenβπΊ) CnP π« π΄)βπ) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)):(BaseβπΊ)βΆπ΄ β§ βπ‘ β π« π΄(((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦))βπ) β π‘ β βπ£ β (TopOpenβπΊ)(π β π£ β§ ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β π£) β π‘))))) |
131 | 36, 125, 130 | mpbir2and 712 |
. . . . . . . . 9
β’ (((π΄ β π β§ π¦ β π΄) β§ π β (BaseβπΊ)) β (π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β (((TopOpenβπΊ) CnP π« π΄)βπ)) |
132 | 131 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π΄ β π β§ π¦ β π΄) β βπ β (BaseβπΊ)(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β (((TopOpenβπΊ) CnP π« π΄)βπ)) |
133 | | cncnp 22654 |
. . . . . . . . . 10
β’
(((TopOpenβπΊ)
β (TopOnβ(BaseβπΊ)) β§ π« π΄ β (TopOnβπ΄)) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β ((TopOpenβπΊ) Cn π« π΄) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)):(BaseβπΊ)βΆπ΄ β§ βπ β (BaseβπΊ)(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β (((TopOpenβπΊ) CnP π« π΄)βπ)))) |
134 | 24, 12, 133 | syl2anc 585 |
. . . . . . . . 9
β’ (π΄ β π β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β ((TopOpenβπΊ) Cn π« π΄) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)):(BaseβπΊ)βΆπ΄ β§ βπ β (BaseβπΊ)(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β (((TopOpenβπΊ) CnP π« π΄)βπ)))) |
135 | 134 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β π β§ π¦ β π΄) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β ((TopOpenβπΊ) Cn π« π΄) β ((π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)):(BaseβπΊ)βΆπ΄ β§ βπ β (BaseβπΊ)(π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β (((TopOpenβπΊ) CnP π« π΄)βπ)))) |
136 | 35, 132, 135 | mpbir2and 712 |
. . . . . . 7
β’ ((π΄ β π β§ π¦ β π΄) β (π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β ((TopOpenβπΊ) Cn π« π΄)) |
137 | | fvconst2g 7155 |
. . . . . . . . 9
β’
((π« π΄ β
Top β§ π¦ β π΄) β ((π΄ Γ {π« π΄})βπ¦) = π« π΄) |
138 | 26, 137 | sylan 581 |
. . . . . . . 8
β’ ((π΄ β π β§ π¦ β π΄) β ((π΄ Γ {π« π΄})βπ¦) = π« π΄) |
139 | 138 | oveq2d 7377 |
. . . . . . 7
β’ ((π΄ β π β§ π¦ β π΄) β ((TopOpenβπΊ) Cn ((π΄ Γ {π« π΄})βπ¦)) = ((TopOpenβπΊ) Cn π« π΄)) |
140 | 136, 139 | eleqtrrd 2837 |
. . . . . 6
β’ ((π΄ β π β§ π¦ β π΄) β (π₯ β (BaseβπΊ) β¦ (β‘π₯βπ¦)) β ((TopOpenβπΊ) Cn ((π΄ Γ {π« π΄})βπ¦))) |
141 | 10, 24, 25, 28, 140 | ptcn 23001 |
. . . . 5
β’ (π΄ β π β (π₯ β (BaseβπΊ) β¦ (π¦ β π΄ β¦ (β‘π₯βπ¦))) β ((TopOpenβπΊ) Cn (βtβ(π΄ Γ {π« π΄})))) |
142 | | eqid 2733 |
. . . . . . . . 9
β’
(invgβπΊ) = (invgβπΊ) |
143 | 5, 142 | grpinvf 18805 |
. . . . . . . 8
β’ (πΊ β Grp β
(invgβπΊ):(BaseβπΊ)βΆ(BaseβπΊ)) |
144 | 2, 143 | syl 17 |
. . . . . . 7
β’ (π΄ β π β (invgβπΊ):(BaseβπΊ)βΆ(BaseβπΊ)) |
145 | 144 | feqmptd 6914 |
. . . . . 6
β’ (π΄ β π β (invgβπΊ) = (π₯ β (BaseβπΊ) β¦ ((invgβπΊ)βπ₯))) |
146 | 1, 5, 142 | symginv 19192 |
. . . . . . . . 9
β’ (π₯ β (BaseβπΊ) β
((invgβπΊ)βπ₯) = β‘π₯) |
147 | 146 | adantl 483 |
. . . . . . . 8
β’ ((π΄ β π β§ π₯ β (BaseβπΊ)) β ((invgβπΊ)βπ₯) = β‘π₯) |
148 | 32 | feqmptd 6914 |
. . . . . . . 8
β’ ((π΄ β π β§ π₯ β (BaseβπΊ)) β β‘π₯ = (π¦ β π΄ β¦ (β‘π₯βπ¦))) |
149 | 147, 148 | eqtrd 2773 |
. . . . . . 7
β’ ((π΄ β π β§ π₯ β (BaseβπΊ)) β ((invgβπΊ)βπ₯) = (π¦ β π΄ β¦ (β‘π₯βπ¦))) |
150 | 149 | mpteq2dva 5209 |
. . . . . 6
β’ (π΄ β π β (π₯ β (BaseβπΊ) β¦ ((invgβπΊ)βπ₯)) = (π₯ β (BaseβπΊ) β¦ (π¦ β π΄ β¦ (β‘π₯βπ¦)))) |
151 | 145, 150 | eqtrd 2773 |
. . . . 5
β’ (π΄ β π β (invgβπΊ) = (π₯ β (BaseβπΊ) β¦ (π¦ β π΄ β¦ (β‘π₯βπ¦)))) |
152 | | xkopt 23029 |
. . . . . . 7
β’
((π« π΄ β
Top β§ π΄ β π) β (π« π΄ βko π«
π΄) =
(βtβ(π΄ Γ {π« π΄}))) |
153 | 26, 152 | mpancom 687 |
. . . . . 6
β’ (π΄ β π β (π« π΄ βko π« π΄) =
(βtβ(π΄ Γ {π« π΄}))) |
154 | 153 | oveq2d 7377 |
. . . . 5
β’ (π΄ β π β ((TopOpenβπΊ) Cn (π« π΄ βko π« π΄)) = ((TopOpenβπΊ) Cn
(βtβ(π΄ Γ {π« π΄})))) |
155 | 141, 151,
154 | 3eltr4d 2849 |
. . . 4
β’ (π΄ β π β (invgβπΊ) β ((TopOpenβπΊ) Cn (π« π΄ βko π«
π΄))) |
156 | | eqid 2733 |
. . . . . . 7
β’
(π« π΄
βko π« π΄) = (π« π΄ βko π« π΄) |
157 | 156 | xkotopon 22974 |
. . . . . 6
β’
((π« π΄ β
Top β§ π« π΄
β Top) β (π« π΄ βko π« π΄) β (TopOnβ(π«
π΄ Cn π« π΄))) |
158 | 26, 26, 157 | syl2anc 585 |
. . . . 5
β’ (π΄ β π β (π« π΄ βko π« π΄) β (TopOnβ(π«
π΄ Cn π« π΄))) |
159 | | frn 6679 |
. . . . . 6
β’
((invgβπΊ):(BaseβπΊ)βΆ(BaseβπΊ) β ran (invgβπΊ) β (BaseβπΊ)) |
160 | 2, 143, 159 | 3syl 18 |
. . . . 5
β’ (π΄ β π β ran (invgβπΊ) β (BaseβπΊ)) |
161 | | cndis 22665 |
. . . . . . 7
β’ ((π΄ β π β§ π« π΄ β (TopOnβπ΄)) β (π« π΄ Cn π« π΄) = (π΄ βm π΄)) |
162 | 12, 161 | mpdan 686 |
. . . . . 6
β’ (π΄ β π β (π« π΄ Cn π« π΄) = (π΄ βm π΄)) |
163 | 21, 162 | sseqtrrd 3989 |
. . . . 5
β’ (π΄ β π β (BaseβπΊ) β (π« π΄ Cn π« π΄)) |
164 | | cnrest2 22660 |
. . . . 5
β’
(((π« π΄
βko π« π΄) β (TopOnβ(π« π΄ Cn π« π΄)) β§ ran (invgβπΊ) β (BaseβπΊ) β§ (BaseβπΊ) β (π« π΄ Cn π« π΄)) β ((invgβπΊ) β ((TopOpenβπΊ) Cn (π« π΄ βko π«
π΄)) β
(invgβπΊ)
β ((TopOpenβπΊ)
Cn ((π« π΄
βko π« π΄) βΎt (BaseβπΊ))))) |
165 | 158, 160,
163, 164 | syl3anc 1372 |
. . . 4
β’ (π΄ β π β ((invgβπΊ) β ((TopOpenβπΊ) Cn (π« π΄ βko π«
π΄)) β
(invgβπΊ)
β ((TopOpenβπΊ)
Cn ((π« π΄
βko π« π΄) βΎt (BaseβπΊ))))) |
166 | 155, 165 | mpbid 231 |
. . 3
β’ (π΄ β π β (invgβπΊ) β ((TopOpenβπΊ) Cn ((π« π΄ βko π«
π΄) βΎt
(BaseβπΊ)))) |
167 | 153 | oveq1d 7376 |
. . . . 5
β’ (π΄ β π β ((π« π΄ βko π« π΄) βΎt
(BaseβπΊ)) =
((βtβ(π΄ Γ {π« π΄})) βΎt (BaseβπΊ))) |
168 | 167, 11 | eqtrd 2773 |
. . . 4
β’ (π΄ β π β ((π« π΄ βko π« π΄) βΎt
(BaseβπΊ)) =
(TopOpenβπΊ)) |
169 | 168 | oveq2d 7377 |
. . 3
β’ (π΄ β π β ((TopOpenβπΊ) Cn ((π« π΄ βko π« π΄) βΎt
(BaseβπΊ))) =
((TopOpenβπΊ) Cn
(TopOpenβπΊ))) |
170 | 166, 169 | eleqtrd 2836 |
. 2
β’ (π΄ β π β (invgβπΊ) β ((TopOpenβπΊ) Cn (TopOpenβπΊ))) |
171 | | eqid 2733 |
. . 3
β’
(TopOpenβπΊ) =
(TopOpenβπΊ) |
172 | 171, 142 | istgp 23451 |
. 2
β’ (πΊ β TopGrp β (πΊ β Grp β§ πΊ β TopMnd β§
(invgβπΊ)
β ((TopOpenβπΊ)
Cn (TopOpenβπΊ)))) |
173 | 2, 9, 170, 172 | syl3anbrc 1344 |
1
β’ (π΄ β π β πΊ β TopGrp) |