Step | Hyp | Ref
| Expression |
1 | | ccfil 24769 |
. 2
class
CauFil |
2 | | vd |
. . 3
setvar π |
3 | | cxmet 20929 |
. . . . 5
class
βMet |
4 | 3 | crn 5678 |
. . . 4
class ran
βMet |
5 | 4 | cuni 4909 |
. . 3
class βͺ ran βMet |
6 | 2 | cv 1541 |
. . . . . . . 8
class π |
7 | | vy |
. . . . . . . . . 10
setvar π¦ |
8 | 7 | cv 1541 |
. . . . . . . . 9
class π¦ |
9 | 8, 8 | cxp 5675 |
. . . . . . . 8
class (π¦ Γ π¦) |
10 | 6, 9 | cima 5680 |
. . . . . . 7
class (π β (π¦ Γ π¦)) |
11 | | cc0 11110 |
. . . . . . . 8
class
0 |
12 | | vx |
. . . . . . . . 9
setvar π₯ |
13 | 12 | cv 1541 |
. . . . . . . 8
class π₯ |
14 | | cico 13326 |
. . . . . . . 8
class
[,) |
15 | 11, 13, 14 | co 7409 |
. . . . . . 7
class
(0[,)π₯) |
16 | 10, 15 | wss 3949 |
. . . . . 6
wff (π β (π¦ Γ π¦)) β (0[,)π₯) |
17 | | vf |
. . . . . . 7
setvar π |
18 | 17 | cv 1541 |
. . . . . 6
class π |
19 | 16, 7, 18 | wrex 3071 |
. . . . 5
wff
βπ¦ β
π (π β (π¦ Γ π¦)) β (0[,)π₯) |
20 | | crp 12974 |
. . . . 5
class
β+ |
21 | 19, 12, 20 | wral 3062 |
. . . 4
wff
βπ₯ β
β+ βπ¦ β π (π β (π¦ Γ π¦)) β (0[,)π₯) |
22 | 6 | cdm 5677 |
. . . . . 6
class dom π |
23 | 22 | cdm 5677 |
. . . . 5
class dom dom
π |
24 | | cfil 23349 |
. . . . 5
class
Fil |
25 | 23, 24 | cfv 6544 |
. . . 4
class
(Filβdom dom π) |
26 | 21, 17, 25 | crab 3433 |
. . 3
class {π β (Filβdom dom π) β£ βπ₯ β β+
βπ¦ β π (π β (π¦ Γ π¦)) β (0[,)π₯)} |
27 | 2, 5, 26 | cmpt 5232 |
. 2
class (π β βͺ ran βMet β¦ {π β (Filβdom dom π) β£ βπ₯ β β+ βπ¦ β π (π β (π¦ Γ π¦)) β (0[,)π₯)}) |
28 | 1, 27 | wceq 1542 |
1
wff CauFil =
(π β βͺ ran βMet β¦ {π β (Filβdom dom π) β£ βπ₯ β β+ βπ¦ β π (π β (π¦ Γ π¦)) β (0[,)π₯)}) |