Step | Hyp | Ref
| Expression |
1 | | ccusp 24022 |
. 2
class
CUnifSp |
2 | | vc |
. . . . . . 7
setvar ๐ |
3 | 2 | cv 1538 |
. . . . . 6
class ๐ |
4 | | vw |
. . . . . . . . 9
setvar ๐ค |
5 | 4 | cv 1538 |
. . . . . . . 8
class ๐ค |
6 | | cuss 23978 |
. . . . . . . 8
class
UnifSt |
7 | 5, 6 | cfv 6542 |
. . . . . . 7
class
(UnifStโ๐ค) |
8 | | ccfilu 24011 |
. . . . . . 7
class
CauFilu |
9 | 7, 8 | cfv 6542 |
. . . . . 6
class
(CauFiluโ(UnifStโ๐ค)) |
10 | 3, 9 | wcel 2104 |
. . . . 5
wff ๐ โ
(CauFiluโ(UnifStโ๐ค)) |
11 | | ctopn 17371 |
. . . . . . . 8
class
TopOpen |
12 | 5, 11 | cfv 6542 |
. . . . . . 7
class
(TopOpenโ๐ค) |
13 | | cflim 23658 |
. . . . . . 7
class
fLim |
14 | 12, 3, 13 | co 7411 |
. . . . . 6
class
((TopOpenโ๐ค)
fLim ๐) |
15 | | c0 4321 |
. . . . . 6
class
โ
|
16 | 14, 15 | wne 2938 |
. . . . 5
wff
((TopOpenโ๐ค)
fLim ๐) โ
โ
|
17 | 10, 16 | wi 4 |
. . . 4
wff (๐ โ
(CauFiluโ(UnifStโ๐ค)) โ ((TopOpenโ๐ค) fLim ๐) โ โ
) |
18 | | cbs 17148 |
. . . . . 6
class
Base |
19 | 5, 18 | cfv 6542 |
. . . . 5
class
(Baseโ๐ค) |
20 | | cfil 23569 |
. . . . 5
class
Fil |
21 | 19, 20 | cfv 6542 |
. . . 4
class
(Filโ(Baseโ๐ค)) |
22 | 17, 2, 21 | wral 3059 |
. . 3
wff
โ๐ โ
(Filโ(Baseโ๐ค))(๐ โ
(CauFiluโ(UnifStโ๐ค)) โ ((TopOpenโ๐ค) fLim ๐) โ โ
) |
23 | | cusp 23979 |
. . 3
class
UnifSp |
24 | 22, 4, 23 | crab 3430 |
. 2
class {๐ค โ UnifSp โฃ
โ๐ โ
(Filโ(Baseโ๐ค))(๐ โ
(CauFiluโ(UnifStโ๐ค)) โ ((TopOpenโ๐ค) fLim ๐) โ โ
)} |
25 | 1, 24 | wceq 1539 |
1
wff CUnifSp =
{๐ค โ UnifSp โฃ
โ๐ โ
(Filโ(Baseโ๐ค))(๐ โ
(CauFiluโ(UnifStโ๐ค)) โ ((TopOpenโ๐ค) fLim ๐) โ โ
)} |