Detailed syntax breakdown of Definition df-eupth
Step | Hyp | Ref
| Expression |
1 | | ceupth 27903 |
. 2
class
EulerPaths |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3492 |
. . 3
class
V |
4 | | vf |
. . . . . . 7
setvar 𝑓 |
5 | 4 | cv 1527 |
. . . . . 6
class 𝑓 |
6 | | vp |
. . . . . . 7
setvar 𝑝 |
7 | 6 | cv 1527 |
. . . . . 6
class 𝑝 |
8 | 2 | cv 1527 |
. . . . . . 7
class 𝑔 |
9 | | ctrls 27399 |
. . . . . . 7
class
Trails |
10 | 8, 9 | cfv 6348 |
. . . . . 6
class
(Trails‘𝑔) |
11 | 5, 7, 10 | wbr 5057 |
. . . . 5
wff 𝑓(Trails‘𝑔)𝑝 |
12 | | cc0 10525 |
. . . . . . 7
class
0 |
13 | | chash 13678 |
. . . . . . . 8
class
♯ |
14 | 5, 13 | cfv 6348 |
. . . . . . 7
class
(♯‘𝑓) |
15 | | cfzo 13021 |
. . . . . . 7
class
..^ |
16 | 12, 14, 15 | co 7145 |
. . . . . 6
class
(0..^(♯‘𝑓)) |
17 | | ciedg 26709 |
. . . . . . . 8
class
iEdg |
18 | 8, 17 | cfv 6348 |
. . . . . . 7
class
(iEdg‘𝑔) |
19 | 18 | cdm 5548 |
. . . . . 6
class dom
(iEdg‘𝑔) |
20 | 16, 19, 5 | wfo 6346 |
. . . . 5
wff 𝑓:(0..^(♯‘𝑓))–onto→dom (iEdg‘𝑔) |
21 | 11, 20 | wa 396 |
. . . 4
wff (𝑓(Trails‘𝑔)𝑝 ∧ 𝑓:(0..^(♯‘𝑓))–onto→dom (iEdg‘𝑔)) |
22 | 21, 4, 6 | copab 5119 |
. . 3
class
{〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝑔)𝑝 ∧ 𝑓:(0..^(♯‘𝑓))–onto→dom (iEdg‘𝑔))} |
23 | 2, 3, 22 | cmpt 5137 |
. 2
class (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝑔)𝑝 ∧ 𝑓:(0..^(♯‘𝑓))–onto→dom (iEdg‘𝑔))}) |
24 | 1, 23 | wceq 1528 |
1
wff EulerPaths
= (𝑔 ∈ V ↦
{〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝑔)𝑝 ∧ 𝑓:(0..^(♯‘𝑓))–onto→dom (iEdg‘𝑔))}) |