Step | Hyp | Ref
| Expression |
1 | | cwwspthsn 29082 |
. 2
class
WSPathsN |
2 | | vn |
. . 3
setvar π |
3 | | vg |
. . 3
setvar π |
4 | | cn0 12472 |
. . 3
class
β0 |
5 | | cvv 3475 |
. . 3
class
V |
6 | | vf |
. . . . . . 7
setvar π |
7 | 6 | cv 1541 |
. . . . . 6
class π |
8 | | vw |
. . . . . . 7
setvar π€ |
9 | 8 | cv 1541 |
. . . . . 6
class π€ |
10 | 3 | cv 1541 |
. . . . . . 7
class π |
11 | | cspths 28970 |
. . . . . . 7
class
SPaths |
12 | 10, 11 | cfv 6544 |
. . . . . 6
class
(SPathsβπ) |
13 | 7, 9, 12 | wbr 5149 |
. . . . 5
wff π(SPathsβπ)π€ |
14 | 13, 6 | wex 1782 |
. . . 4
wff
βπ π(SPathsβπ)π€ |
15 | 2 | cv 1541 |
. . . . 5
class π |
16 | | cwwlksn 29080 |
. . . . 5
class
WWalksN |
17 | 15, 10, 16 | co 7409 |
. . . 4
class (π WWalksN π) |
18 | 14, 8, 17 | crab 3433 |
. . 3
class {π€ β (π WWalksN π) β£ βπ π(SPathsβπ)π€} |
19 | 2, 3, 4, 5, 18 | cmpo 7411 |
. 2
class (π β β0,
π β V β¦ {π€ β (π WWalksN π) β£ βπ π(SPathsβπ)π€}) |
20 | 1, 19 | wceq 1542 |
1
wff WSPathsN =
(π β
β0, π
β V β¦ {π€ β
(π WWalksN π) β£ βπ π(SPathsβπ)π€}) |