Step | Hyp | Ref
| Expression |
1 | | ceupth 29450 |
. 2
class
EulerPaths |
2 | | vg |
. . 3
setvar π |
3 | | cvv 3475 |
. . 3
class
V |
4 | | vf |
. . . . . . 7
setvar π |
5 | 4 | cv 1541 |
. . . . . 6
class π |
6 | | vp |
. . . . . . 7
setvar π |
7 | 6 | cv 1541 |
. . . . . 6
class π |
8 | 2 | cv 1541 |
. . . . . . 7
class π |
9 | | ctrls 28947 |
. . . . . . 7
class
Trails |
10 | 8, 9 | cfv 6544 |
. . . . . 6
class
(Trailsβπ) |
11 | 5, 7, 10 | wbr 5149 |
. . . . 5
wff π(Trailsβπ)π |
12 | | cc0 11110 |
. . . . . . 7
class
0 |
13 | | chash 14290 |
. . . . . . . 8
class
β― |
14 | 5, 13 | cfv 6544 |
. . . . . . 7
class
(β―βπ) |
15 | | cfzo 13627 |
. . . . . . 7
class
..^ |
16 | 12, 14, 15 | co 7409 |
. . . . . 6
class
(0..^(β―βπ)) |
17 | | ciedg 28257 |
. . . . . . . 8
class
iEdg |
18 | 8, 17 | cfv 6544 |
. . . . . . 7
class
(iEdgβπ) |
19 | 18 | cdm 5677 |
. . . . . 6
class dom
(iEdgβπ) |
20 | 16, 19, 5 | wfo 6542 |
. . . . 5
wff π:(0..^(β―βπ))βontoβdom (iEdgβπ) |
21 | 11, 20 | wa 397 |
. . . 4
wff (π(Trailsβπ)π β§ π:(0..^(β―βπ))βontoβdom (iEdgβπ)) |
22 | 21, 4, 6 | copab 5211 |
. . 3
class
{β¨π, πβ© β£ (π(Trailsβπ)π β§ π:(0..^(β―βπ))βontoβdom (iEdgβπ))} |
23 | 2, 3, 22 | cmpt 5232 |
. 2
class (π β V β¦ {β¨π, πβ© β£ (π(Trailsβπ)π β§ π:(0..^(β―βπ))βontoβdom (iEdgβπ))}) |
24 | 1, 23 | wceq 1542 |
1
wff EulerPaths
= (π β V β¦
{β¨π, πβ© β£ (π(Trailsβπ)π β§ π:(0..^(β―βπ))βontoβdom (iEdgβπ))}) |