Step | Hyp | Ref
| Expression |
1 | | cmntop 32997 |
. 2
class
ManTop |
2 | | vn |
. . . . . 6
setvar π |
3 | 2 | cv 1540 |
. . . . 5
class π |
4 | | cn0 12471 |
. . . . 5
class
β0 |
5 | 3, 4 | wcel 2106 |
. . . 4
wff π β
β0 |
6 | | vj |
. . . . . . 7
setvar π |
7 | 6 | cv 1540 |
. . . . . 6
class π |
8 | | c2ndc 22941 |
. . . . . 6
class
2ndΟ |
9 | 7, 8 | wcel 2106 |
. . . . 5
wff π β
2ndΟ |
10 | | cha 22811 |
. . . . . 6
class
Haus |
11 | 7, 10 | wcel 2106 |
. . . . 5
wff π β Haus |
12 | | cehl 24900 |
. . . . . . . . . 10
class
πΌhil |
13 | 3, 12 | cfv 6543 |
. . . . . . . . 9
class
(πΌhilβπ) |
14 | | ctopn 17366 |
. . . . . . . . 9
class
TopOpen |
15 | 13, 14 | cfv 6543 |
. . . . . . . 8
class
(TopOpenβ(πΌhilβπ)) |
16 | | chmph 23257 |
. . . . . . . 8
class
β |
17 | 15, 16 | cec 8700 |
. . . . . . 7
class
[(TopOpenβ(πΌhilβπ))] β |
18 | 17 | clly 22967 |
. . . . . 6
class Locally
[(TopOpenβ(πΌhilβπ))] β |
19 | 7, 18 | wcel 2106 |
. . . . 5
wff π β Locally
[(TopOpenβ(πΌhilβπ))] β |
20 | 9, 11, 19 | w3a 1087 |
. . . 4
wff (π β 2ndΟ
β§ π β Haus β§
π β Locally
[(TopOpenβ(πΌhilβπ))] β ) |
21 | 5, 20 | wa 396 |
. . 3
wff (π β β0
β§ (π β
2ndΟ β§ π β Haus β§ π β Locally
[(TopOpenβ(πΌhilβπ))] β )) |
22 | 21, 2, 6 | copab 5210 |
. 2
class
{β¨π, πβ© β£ (π β β0
β§ (π β
2ndΟ β§ π β Haus β§ π β Locally
[(TopOpenβ(πΌhilβπ))] β ))} |
23 | 1, 22 | wceq 1541 |
1
wff ManTop =
{β¨π, πβ© β£ (π β β0
β§ (π β
2ndΟ β§ π β Haus β§ π β Locally
[(TopOpenβ(πΌhilβπ))] β ))} |