Step | Hyp | Ref
| Expression |
1 | | cwwspthsnon 29121 |
. 2
class
WSPathsNOn |
2 | | vn |
. . 3
setvar π |
3 | | vg |
. . 3
setvar π |
4 | | cn0 12474 |
. . 3
class
β0 |
5 | | cvv 3474 |
. . 3
class
V |
6 | | va |
. . . 4
setvar π |
7 | | vb |
. . . 4
setvar π |
8 | 3 | cv 1540 |
. . . . 5
class π |
9 | | cvtx 28294 |
. . . . 5
class
Vtx |
10 | 8, 9 | cfv 6543 |
. . . 4
class
(Vtxβπ) |
11 | | vf |
. . . . . . . 8
setvar π |
12 | 11 | cv 1540 |
. . . . . . 7
class π |
13 | | vw |
. . . . . . . 8
setvar π€ |
14 | 13 | cv 1540 |
. . . . . . 7
class π€ |
15 | 6 | cv 1540 |
. . . . . . . 8
class π |
16 | 7 | cv 1540 |
. . . . . . . 8
class π |
17 | | cspthson 29010 |
. . . . . . . . 9
class
SPathsOn |
18 | 8, 17 | cfv 6543 |
. . . . . . . 8
class
(SPathsOnβπ) |
19 | 15, 16, 18 | co 7411 |
. . . . . . 7
class (π(SPathsOnβπ)π) |
20 | 12, 14, 19 | wbr 5148 |
. . . . . 6
wff π(π(SPathsOnβπ)π)π€ |
21 | 20, 11 | wex 1781 |
. . . . 5
wff
βπ π(π(SPathsOnβπ)π)π€ |
22 | 2 | cv 1540 |
. . . . . . 7
class π |
23 | | cwwlksnon 29119 |
. . . . . . 7
class
WWalksNOn |
24 | 22, 8, 23 | co 7411 |
. . . . . 6
class (π WWalksNOn π) |
25 | 15, 16, 24 | co 7411 |
. . . . 5
class (π(π WWalksNOn π)π) |
26 | 21, 13, 25 | crab 3432 |
. . . 4
class {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€} |
27 | 6, 7, 10, 10, 26 | cmpo 7413 |
. . 3
class (π β (Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€}) |
28 | 2, 3, 4, 5, 27 | cmpo 7413 |
. 2
class (π β β0,
π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€})) |
29 | 1, 28 | wceq 1541 |
1
wff WSPathsNOn
= (π β
β0, π
β V β¦ (π β
(Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€})) |