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 29451
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 29450 . 2 class EulerPaths
2 vg . . 3 setvar 𝑔
3 cvv 3475 . . 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 28947 . . . . . . 7 class Trails
108, 9cfv 6544 . . . . . 6 class (Trailsβ€˜π‘”)
115, 7, 10wbr 5149 . . . . 5 wff 𝑓(Trailsβ€˜π‘”)𝑝
12 cc0 11110 . . . . . . 7 class 0
13 chash 14290 . . . . . . . 8 class β™―
145, 13cfv 6544 . . . . . . 7 class (β™―β€˜π‘“)
15 cfzo 13627 . . . . . . 7 class ..^
1612, 14, 15co 7409 . . . . . 6 class (0..^(β™―β€˜π‘“))
17 ciedg 28257 . . . . . . . 8 class iEdg
188, 17cfv 6544 . . . . . . 7 class (iEdgβ€˜π‘”)
1918cdm 5677 . . . . . 6 class dom (iEdgβ€˜π‘”)
2016, 19, 5wfo 6542 . . . . 5 wff 𝑓:(0..^(β™―β€˜π‘“))–ontoβ†’dom (iEdgβ€˜π‘”)
2111, 20wa 397 . . . 4 wff (𝑓(Trailsβ€˜π‘”)𝑝 ∧ 𝑓:(0..^(β™―β€˜π‘“))–ontoβ†’dom (iEdgβ€˜π‘”))
2221, 4, 6copab 5211 . . 3 class {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(Trailsβ€˜π‘”)𝑝 ∧ 𝑓:(0..^(β™―β€˜π‘“))–ontoβ†’dom (iEdgβ€˜π‘”))}
232, 3, 22cmpt 5232 . 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  29452  eupths  29453
  Copyright terms: Public domain W3C validator