Step | Hyp | Ref
| Expression |
1 | | ctotbnd 36634 |
. 2
class
TotBnd |
2 | | vx |
. . 3
setvar π₯ |
3 | | cvv 3475 |
. . 3
class
V |
4 | | vv |
. . . . . . . . . 10
setvar π£ |
5 | 4 | cv 1541 |
. . . . . . . . 9
class π£ |
6 | 5 | cuni 4909 |
. . . . . . . 8
class βͺ π£ |
7 | 2 | cv 1541 |
. . . . . . . 8
class π₯ |
8 | 6, 7 | wceq 1542 |
. . . . . . 7
wff βͺ π£ =
π₯ |
9 | | vb |
. . . . . . . . . . 11
setvar π |
10 | 9 | cv 1541 |
. . . . . . . . . 10
class π |
11 | | vy |
. . . . . . . . . . . 12
setvar π¦ |
12 | 11 | cv 1541 |
. . . . . . . . . . 11
class π¦ |
13 | | vd |
. . . . . . . . . . . 12
setvar π |
14 | 13 | cv 1541 |
. . . . . . . . . . 11
class π |
15 | | vm |
. . . . . . . . . . . . 13
setvar π |
16 | 15 | cv 1541 |
. . . . . . . . . . . 12
class π |
17 | | cbl 20931 |
. . . . . . . . . . . 12
class
ball |
18 | 16, 17 | cfv 6544 |
. . . . . . . . . . 11
class
(ballβπ) |
19 | 12, 14, 18 | co 7409 |
. . . . . . . . . 10
class (π¦(ballβπ)π) |
20 | 10, 19 | wceq 1542 |
. . . . . . . . 9
wff π = (π¦(ballβπ)π) |
21 | 20, 11, 7 | wrex 3071 |
. . . . . . . 8
wff
βπ¦ β
π₯ π = (π¦(ballβπ)π) |
22 | 21, 9, 5 | wral 3062 |
. . . . . . 7
wff
βπ β
π£ βπ¦ β π₯ π = (π¦(ballβπ)π) |
23 | 8, 22 | wa 397 |
. . . . . 6
wff (βͺ π£ =
π₯ β§ βπ β π£ βπ¦ β π₯ π = (π¦(ballβπ)π)) |
24 | | cfn 8939 |
. . . . . 6
class
Fin |
25 | 23, 4, 24 | wrex 3071 |
. . . . 5
wff
βπ£ β Fin
(βͺ π£ = π₯ β§ βπ β π£ βπ¦ β π₯ π = (π¦(ballβπ)π)) |
26 | | crp 12974 |
. . . . 5
class
β+ |
27 | 25, 13, 26 | wral 3062 |
. . . 4
wff
βπ β
β+ βπ£ β Fin (βͺ
π£ = π₯ β§ βπ β π£ βπ¦ β π₯ π = (π¦(ballβπ)π)) |
28 | | cmet 20930 |
. . . . 5
class
Met |
29 | 7, 28 | cfv 6544 |
. . . 4
class
(Metβπ₯) |
30 | 27, 15, 29 | crab 3433 |
. . 3
class {π β (Metβπ₯) β£ βπ β β+
βπ£ β Fin (βͺ π£ =
π₯ β§ βπ β π£ βπ¦ β π₯ π = (π¦(ballβπ)π))} |
31 | 2, 3, 30 | cmpt 5232 |
. 2
class (π₯ β V β¦ {π β (Metβπ₯) β£ βπ β β+
βπ£ β Fin (βͺ π£ =
π₯ β§ βπ β π£ βπ¦ β π₯ π = (π¦(ballβπ)π))}) |
32 | 1, 31 | wceq 1542 |
1
wff TotBnd =
(π₯ β V β¦ {π β (Metβπ₯) β£ βπ β β+
βπ£ β Fin (βͺ π£ =
π₯ β§ βπ β π£ βπ¦ β π₯ π = (π¦(ballβπ)π))}) |