MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-eupth Structured version   Visualization version   GIF version

Definition df-eupth 29145
Description: Define the set of all Eulerian paths on an arbitrary graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
Assertion
Ref Expression
df-eupth EulerPaths = (𝑔 ∈ V ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(Trailsβ€˜π‘”)𝑝 ∧ 𝑓:(0..^(β™―β€˜π‘“))–ontoβ†’dom (iEdgβ€˜π‘”))})
Distinct variable group:   𝑓,𝑔,𝑝

Detailed syntax breakdown of Definition df-eupth
StepHypRef Expression
1 ceupth 29144 . 2 class EulerPaths
2 vg . . 3 setvar 𝑔
3 cvv 3446 . . 3 class V
4 vf . . . . . . 7 setvar 𝑓
54cv 1541 . . . . . 6 class 𝑓
6 vp . . . . . . 7 setvar 𝑝
76cv 1541 . . . . . 6 class 𝑝
82cv 1541 . . . . . . 7 class 𝑔
9 ctrls 28641 . . . . . . 7 class Trails
108, 9cfv 6497 . . . . . 6 class (Trailsβ€˜π‘”)
115, 7, 10wbr 5106 . . . . 5 wff 𝑓(Trailsβ€˜π‘”)𝑝
12 cc0 11052 . . . . . . 7 class 0
13 chash 14231 . . . . . . . 8 class β™―
145, 13cfv 6497 . . . . . . 7 class (β™―β€˜π‘“)
15 cfzo 13568 . . . . . . 7 class ..^
1612, 14, 15co 7358 . . . . . 6 class (0..^(β™―β€˜π‘“))
17 ciedg 27951 . . . . . . . 8 class iEdg
188, 17cfv 6497 . . . . . . 7 class (iEdgβ€˜π‘”)
1918cdm 5634 . . . . . 6 class dom (iEdgβ€˜π‘”)
2016, 19, 5wfo 6495 . . . . 5 wff 𝑓:(0..^(β™―β€˜π‘“))–ontoβ†’dom (iEdgβ€˜π‘”)
2111, 20wa 397 . . . 4 wff (𝑓(Trailsβ€˜π‘”)𝑝 ∧ 𝑓:(0..^(β™―β€˜π‘“))–ontoβ†’dom (iEdgβ€˜π‘”))
2221, 4, 6copab 5168 . . 3 class {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(Trailsβ€˜π‘”)𝑝 ∧ 𝑓:(0..^(β™―β€˜π‘“))–ontoβ†’dom (iEdgβ€˜π‘”))}
232, 3, 22cmpt 5189 . 2 class (𝑔 ∈ V ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(Trailsβ€˜π‘”)𝑝 ∧ 𝑓:(0..^(β™―β€˜π‘“))–ontoβ†’dom (iEdgβ€˜π‘”))})
241, 23wceq 1542 1 wff EulerPaths = (𝑔 ∈ V ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(Trailsβ€˜π‘”)𝑝 ∧ 𝑓:(0..^(β™―β€˜π‘“))–ontoβ†’dom (iEdgβ€˜π‘”))})
Colors of variables: wff setvar class
This definition is referenced by:  releupth  29146  eupths  29147
  Copyright terms: Public domain W3C validator