Step | Hyp | Ref
| Expression |
1 | | ctgp 23438 |
. 2
class
TopGrp |
2 | | vf |
. . . . . . 7
setvar π |
3 | 2 | cv 1541 |
. . . . . 6
class π |
4 | | cminusg 18756 |
. . . . . 6
class
invg |
5 | 3, 4 | cfv 6501 |
. . . . 5
class
(invgβπ) |
6 | | vj |
. . . . . . 7
setvar π |
7 | 6 | cv 1541 |
. . . . . 6
class π |
8 | | ccn 22591 |
. . . . . 6
class
Cn |
9 | 7, 7, 8 | co 7362 |
. . . . 5
class (π Cn π) |
10 | 5, 9 | wcel 2107 |
. . . 4
wff
(invgβπ) β (π Cn π) |
11 | | ctopn 17310 |
. . . . 5
class
TopOpen |
12 | 3, 11 | cfv 6501 |
. . . 4
class
(TopOpenβπ) |
13 | 10, 6, 12 | wsbc 3744 |
. . 3
wff
[(TopOpenβπ) / π](invgβπ) β (π Cn π) |
14 | | cgrp 18755 |
. . . 4
class
Grp |
15 | | ctmd 23437 |
. . . 4
class
TopMnd |
16 | 14, 15 | cin 3914 |
. . 3
class (Grp
β© TopMnd) |
17 | 13, 2, 16 | crab 3410 |
. 2
class {π β (Grp β© TopMnd)
β£ [(TopOpenβπ) / π](invgβπ) β (π Cn π)} |
18 | 1, 17 | wceq 1542 |
1
wff TopGrp =
{π β (Grp β©
TopMnd) β£ [(TopOpenβπ) / π](invgβπ) β (π Cn π)} |