Step | Hyp | Ref
| Expression |
1 | | ccmet 24771 |
. 2
class
CMet |
2 | | vx |
. . 3
setvar π₯ |
3 | | cvv 3475 |
. . 3
class
V |
4 | | vd |
. . . . . . . . 9
setvar π |
5 | 4 | cv 1541 |
. . . . . . . 8
class π |
6 | | cmopn 20934 |
. . . . . . . 8
class
MetOpen |
7 | 5, 6 | cfv 6544 |
. . . . . . 7
class
(MetOpenβπ) |
8 | | vf |
. . . . . . . 8
setvar π |
9 | 8 | cv 1541 |
. . . . . . 7
class π |
10 | | cflim 23438 |
. . . . . . 7
class
fLim |
11 | 7, 9, 10 | co 7409 |
. . . . . 6
class
((MetOpenβπ)
fLim π) |
12 | | c0 4323 |
. . . . . 6
class
β
|
13 | 11, 12 | wne 2941 |
. . . . 5
wff
((MetOpenβπ)
fLim π) β
β
|
14 | | ccfil 24769 |
. . . . . 6
class
CauFil |
15 | 5, 14 | cfv 6544 |
. . . . 5
class
(CauFilβπ) |
16 | 13, 8, 15 | wral 3062 |
. . . 4
wff
βπ β
(CauFilβπ)((MetOpenβπ) fLim π) β β
|
17 | 2 | cv 1541 |
. . . . 5
class π₯ |
18 | | cmet 20930 |
. . . . 5
class
Met |
19 | 17, 18 | cfv 6544 |
. . . 4
class
(Metβπ₯) |
20 | 16, 4, 19 | crab 3433 |
. . 3
class {π β (Metβπ₯) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
} |
21 | 2, 3, 20 | cmpt 5232 |
. 2
class (π₯ β V β¦ {π β (Metβπ₯) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
}) |
22 | 1, 21 | wceq 1542 |
1
wff CMet =
(π₯ β V β¦ {π β (Metβπ₯) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
}) |