Step | Hyp | Ref
| Expression |
1 | | ctmd 23437 |
. 2
class
TopMnd |
2 | | vf |
. . . . . . 7
setvar π |
3 | 2 | cv 1541 |
. . . . . 6
class π |
4 | | cplusf 18501 |
. . . . . 6
class
+π |
5 | 3, 4 | cfv 6501 |
. . . . 5
class
(+πβπ) |
6 | | vj |
. . . . . . . 8
setvar π |
7 | 6 | cv 1541 |
. . . . . . 7
class π |
8 | | ctx 22927 |
. . . . . . 7
class
Γt |
9 | 7, 7, 8 | co 7362 |
. . . . . 6
class (π Γt π) |
10 | | ccn 22591 |
. . . . . 6
class
Cn |
11 | 9, 7, 10 | co 7362 |
. . . . 5
class ((π Γt π) Cn π) |
12 | 5, 11 | wcel 2107 |
. . . 4
wff
(+πβπ) β ((π Γt π) Cn π) |
13 | | ctopn 17310 |
. . . . 5
class
TopOpen |
14 | 3, 13 | cfv 6501 |
. . . 4
class
(TopOpenβπ) |
15 | 12, 6, 14 | wsbc 3744 |
. . 3
wff
[(TopOpenβπ) / π](+πβπ) β ((π Γt π) Cn π) |
16 | | cmnd 18563 |
. . . 4
class
Mnd |
17 | | ctps 22297 |
. . . 4
class
TopSp |
18 | 16, 17 | cin 3914 |
. . 3
class (Mnd
β© TopSp) |
19 | 15, 2, 18 | crab 3410 |
. 2
class {π β (Mnd β© TopSp)
β£ [(TopOpenβπ) / π](+πβπ) β ((π Γt π) Cn π)} |
20 | 1, 19 | wceq 1542 |
1
wff TopMnd =
{π β (Mnd β© TopSp)
β£ [(TopOpenβπ) / π](+πβπ) β ((π Γt π) Cn π)} |