Step | Hyp | Ref
| Expression |
1 | | ccau 25168 |
. 2
class
Cau |
2 | | vd |
. . 3
setvar π |
3 | | cxmet 21251 |
. . . . 5
class
βMet |
4 | 3 | crn 5673 |
. . . 4
class ran
βMet |
5 | 4 | cuni 4903 |
. . 3
class βͺ ran βMet |
6 | | vj |
. . . . . . . . 9
setvar π |
7 | 6 | cv 1533 |
. . . . . . . 8
class π |
8 | | cuz 12844 |
. . . . . . . 8
class
β€β₯ |
9 | 7, 8 | cfv 6542 |
. . . . . . 7
class
(β€β₯βπ) |
10 | | vf |
. . . . . . . . . 10
setvar π |
11 | 10 | cv 1533 |
. . . . . . . . 9
class π |
12 | 7, 11 | cfv 6542 |
. . . . . . . 8
class (πβπ) |
13 | | vx |
. . . . . . . . 9
setvar π₯ |
14 | 13 | cv 1533 |
. . . . . . . 8
class π₯ |
15 | 2 | cv 1533 |
. . . . . . . . 9
class π |
16 | | cbl 21253 |
. . . . . . . . 9
class
ball |
17 | 15, 16 | cfv 6542 |
. . . . . . . 8
class
(ballβπ) |
18 | 12, 14, 17 | co 7414 |
. . . . . . 7
class ((πβπ)(ballβπ)π₯) |
19 | 11, 9 | cres 5674 |
. . . . . . 7
class (π βΎ
(β€β₯βπ)) |
20 | 9, 18, 19 | wf 6538 |
. . . . . 6
wff (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯) |
21 | | cz 12580 |
. . . . . 6
class
β€ |
22 | 20, 6, 21 | wrex 3065 |
. . . . 5
wff
βπ β
β€ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯) |
23 | | crp 12998 |
. . . . 5
class
β+ |
24 | 22, 13, 23 | wral 3056 |
. . . 4
wff
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯) |
25 | 15 | cdm 5672 |
. . . . . 6
class dom π |
26 | 25 | cdm 5672 |
. . . . 5
class dom dom
π |
27 | | cc 11128 |
. . . . 5
class
β |
28 | | cpm 8837 |
. . . . 5
class
βpm |
29 | 26, 27, 28 | co 7414 |
. . . 4
class (dom dom
π βpm
β) |
30 | 24, 10, 29 | crab 3427 |
. . 3
class {π β (dom dom π βpm β)
β£ βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯)} |
31 | 2, 5, 30 | cmpt 5225 |
. 2
class (π β βͺ ran βMet β¦ {π β (dom dom π βpm β) β£
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯)}) |
32 | 1, 31 | wceq 1534 |
1
wff Cau =
(π β βͺ ran βMet β¦ {π β (dom dom π βpm β) β£
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯)}) |