Step | Hyp | Ref
| Expression |
1 | | cclwwlknon 29080 |
. 2
class
ClWWalksNOn |
2 | | vg |
. . 3
setvar π |
3 | | cvv 3447 |
. . 3
class
V |
4 | | vv |
. . . 4
setvar π£ |
5 | | vn |
. . . 4
setvar π |
6 | 2 | cv 1541 |
. . . . 5
class π |
7 | | cvtx 27996 |
. . . . 5
class
Vtx |
8 | 6, 7 | cfv 6500 |
. . . 4
class
(Vtxβπ) |
9 | | cn0 12421 |
. . . 4
class
β0 |
10 | | cc0 11059 |
. . . . . . 7
class
0 |
11 | | vw |
. . . . . . . 8
setvar π€ |
12 | 11 | cv 1541 |
. . . . . . 7
class π€ |
13 | 10, 12 | cfv 6500 |
. . . . . 6
class (π€β0) |
14 | 4 | cv 1541 |
. . . . . 6
class π£ |
15 | 13, 14 | wceq 1542 |
. . . . 5
wff (π€β0) = π£ |
16 | 5 | cv 1541 |
. . . . . 6
class π |
17 | | cclwwlkn 29017 |
. . . . . 6
class
ClWWalksN |
18 | 16, 6, 17 | co 7361 |
. . . . 5
class (π ClWWalksN π) |
19 | 15, 11, 18 | crab 3406 |
. . . 4
class {π€ β (π ClWWalksN π) β£ (π€β0) = π£} |
20 | 4, 5, 8, 9, 19 | cmpo 7363 |
. . 3
class (π£ β (Vtxβπ), π β β0 β¦ {π€ β (π ClWWalksN π) β£ (π€β0) = π£}) |
21 | 2, 3, 20 | cmpt 5192 |
. 2
class (π β V β¦ (π£ β (Vtxβπ), π β β0 β¦ {π€ β (π ClWWalksN π) β£ (π€β0) = π£})) |
22 | 1, 21 | wceq 1542 |
1
wff ClWWalksNOn
= (π β V β¦
(π£ β (Vtxβπ), π β β0 β¦ {π€ β (π ClWWalksN π) β£ (π€β0) = π£})) |