Step | Hyp | Ref
| Expression |
1 | | cwlkson 28851 |
. 2
class
WalksOn |
2 | | vg |
. . 3
setvar π |
3 | | cvv 3474 |
. . 3
class
V |
4 | | va |
. . . 4
setvar π |
5 | | vb |
. . . 4
setvar π |
6 | 2 | cv 1540 |
. . . . 5
class π |
7 | | cvtx 28253 |
. . . . 5
class
Vtx |
8 | 6, 7 | cfv 6543 |
. . . 4
class
(Vtxβπ) |
9 | | vf |
. . . . . . . 8
setvar π |
10 | 9 | cv 1540 |
. . . . . . 7
class π |
11 | | vp |
. . . . . . . 8
setvar π |
12 | 11 | cv 1540 |
. . . . . . 7
class π |
13 | | cwlks 28850 |
. . . . . . . 8
class
Walks |
14 | 6, 13 | cfv 6543 |
. . . . . . 7
class
(Walksβπ) |
15 | 10, 12, 14 | wbr 5148 |
. . . . . 6
wff π(Walksβπ)π |
16 | | cc0 11109 |
. . . . . . . 8
class
0 |
17 | 16, 12 | cfv 6543 |
. . . . . . 7
class (πβ0) |
18 | 4 | cv 1540 |
. . . . . . 7
class π |
19 | 17, 18 | wceq 1541 |
. . . . . 6
wff (πβ0) = π |
20 | | chash 14289 |
. . . . . . . . 9
class
β― |
21 | 10, 20 | cfv 6543 |
. . . . . . . 8
class
(β―βπ) |
22 | 21, 12 | cfv 6543 |
. . . . . . 7
class (πβ(β―βπ)) |
23 | 5 | cv 1540 |
. . . . . . 7
class π |
24 | 22, 23 | wceq 1541 |
. . . . . 6
wff (πβ(β―βπ)) = π |
25 | 15, 19, 24 | w3a 1087 |
. . . . 5
wff (π(Walksβπ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π) |
26 | 25, 9, 11 | copab 5210 |
. . . 4
class
{β¨π, πβ© β£ (π(Walksβπ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π)} |
27 | 4, 5, 8, 8, 26 | cmpo 7410 |
. . 3
class (π β (Vtxβπ), π β (Vtxβπ) β¦ {β¨π, πβ© β£ (π(Walksβπ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π)}) |
28 | 2, 3, 27 | cmpt 5231 |
. 2
class (π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {β¨π, πβ© β£ (π(Walksβπ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π)})) |
29 | 1, 28 | wceq 1541 |
1
wff WalksOn =
(π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {β¨π, πβ© β£ (π(Walksβπ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π)})) |