Step | Hyp | Ref
| Expression |
1 | | ccms 24699 |
. 2
class
CMetSp |
2 | | vw |
. . . . . . . 8
setvar π€ |
3 | 2 | cv 1541 |
. . . . . . 7
class π€ |
4 | | cds 17143 |
. . . . . . 7
class
dist |
5 | 3, 4 | cfv 6497 |
. . . . . 6
class
(distβπ€) |
6 | | vb |
. . . . . . . 8
setvar π |
7 | 6 | cv 1541 |
. . . . . . 7
class π |
8 | 7, 7 | cxp 5632 |
. . . . . 6
class (π Γ π) |
9 | 5, 8 | cres 5636 |
. . . . 5
class
((distβπ€)
βΎ (π Γ π)) |
10 | | ccmet 24621 |
. . . . . 6
class
CMet |
11 | 7, 10 | cfv 6497 |
. . . . 5
class
(CMetβπ) |
12 | 9, 11 | wcel 2107 |
. . . 4
wff
((distβπ€)
βΎ (π Γ π)) β (CMetβπ) |
13 | | cbs 17084 |
. . . . 5
class
Base |
14 | 3, 13 | cfv 6497 |
. . . 4
class
(Baseβπ€) |
15 | 12, 6, 14 | wsbc 3740 |
. . 3
wff
[(Baseβπ€) / π]((distβπ€) βΎ (π Γ π)) β (CMetβπ) |
16 | | cms 23674 |
. . 3
class
MetSp |
17 | 15, 2, 16 | crab 3408 |
. 2
class {π€ β MetSp β£
[(Baseβπ€) /
π]((distβπ€) βΎ (π Γ π)) β (CMetβπ)} |
18 | 1, 17 | wceq 1542 |
1
wff CMetSp =
{π€ β MetSp β£
[(Baseβπ€) /
π]((distβπ€) βΎ (π Γ π)) β (CMetβπ)} |