Detailed syntax breakdown of Definition df-eupth
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ceupth 41364 |
. 2
class
EulerPaths |
| 2 | | vg |
. . 3
setvar 𝑔 |
| 3 | | cvv 3173 |
. . 3
class
V |
| 4 | | vf |
. . . . . . 7
setvar 𝑓 |
| 5 | 4 | cv 1474 |
. . . . . 6
class 𝑓 |
| 6 | | vp |
. . . . . . 7
setvar 𝑝 |
| 7 | 6 | cv 1474 |
. . . . . 6
class 𝑝 |
| 8 | 2 | cv 1474 |
. . . . . . 7
class 𝑔 |
| 9 | | ctrls 40899 |
. . . . . . 7
class
TrailS |
| 10 | 8, 9 | cfv 5804 |
. . . . . 6
class
(TrailS‘𝑔) |
| 11 | 5, 7, 10 | wbr 4583 |
. . . . 5
wff 𝑓(TrailS‘𝑔)𝑝 |
| 12 | | cc0 9815 |
. . . . . . 7
class
0 |
| 13 | | chash 12979 |
. . . . . . . 8
class
# |
| 14 | 5, 13 | cfv 5804 |
. . . . . . 7
class
(#‘𝑓) |
| 15 | | cfzo 12334 |
. . . . . . 7
class
..^ |
| 16 | 12, 14, 15 | co 6549 |
. . . . . 6
class
(0..^(#‘𝑓)) |
| 17 | | ciedg 25674 |
. . . . . . . 8
class
iEdg |
| 18 | 8, 17 | cfv 5804 |
. . . . . . 7
class
(iEdg‘𝑔) |
| 19 | 18 | cdm 5038 |
. . . . . 6
class dom
(iEdg‘𝑔) |
| 20 | 16, 19, 5 | wfo 5802 |
. . . . 5
wff 𝑓:(0..^(#‘𝑓))–onto→dom (iEdg‘𝑔) |
| 21 | 11, 20 | wa 383 |
. . . 4
wff (𝑓(TrailS‘𝑔)𝑝 ∧ 𝑓:(0..^(#‘𝑓))–onto→dom (iEdg‘𝑔)) |
| 22 | 21, 4, 6 | copab 4642 |
. . 3
class
{⟨𝑓, 𝑝⟩ ∣ (𝑓(TrailS‘𝑔)𝑝 ∧ 𝑓:(0..^(#‘𝑓))–onto→dom (iEdg‘𝑔))} |
| 23 | 2, 3, 22 | cmpt 4643 |
. 2
class (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(TrailS‘𝑔)𝑝 ∧ 𝑓:(0..^(#‘𝑓))–onto→dom (iEdg‘𝑔))}) |
| 24 | 1, 23 | wceq 1475 |
1
wff EulerPaths
= (𝑔 ∈ V ↦
{⟨𝑓, 𝑝⟩ ∣ (𝑓(TrailS‘𝑔)𝑝 ∧ 𝑓:(0..^(#‘𝑓))–onto→dom (iEdg‘𝑔))}) |
