Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-eupth Structured version   Visualization version   GIF version

Definition df-eupth 41363
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 41362 . 2 class EulerPaths
2 vg . . 3 setvar 𝑔
3 cvv 3168 . . 3 class V
4 vf . . . . . . 7 setvar 𝑓
54cv 1473 . . . . . 6 class 𝑓
6 vp . . . . . . 7 setvar 𝑝
76cv 1473 . . . . . 6 class 𝑝
82cv 1473 . . . . . . 7 class 𝑔
9 ctrls 40897 . . . . . . 7 class TrailS
108, 9cfv 5786 . . . . . 6 class (TrailS‘𝑔)
115, 7, 10wbr 4573 . . . . 5 wff 𝑓(TrailS‘𝑔)𝑝
12 cc0 9788 . . . . . . 7 class 0
13 chash 12930 . . . . . . . 8 class #
145, 13cfv 5786 . . . . . . 7 class (#‘𝑓)
15 cfzo 12285 . . . . . . 7 class ..^
1612, 14, 15co 6523 . . . . . 6 class (0..^(#‘𝑓))
17 ciedg 40228 . . . . . . . 8 class iEdg
188, 17cfv 5786 . . . . . . 7 class (iEdg‘𝑔)
1918cdm 5024 . . . . . 6 class dom (iEdg‘𝑔)
2016, 19, 5wfo 5784 . . . . 5 wff 𝑓:(0..^(#‘𝑓))–onto→dom (iEdg‘𝑔)
2111, 20wa 382 . . . 4 wff (𝑓(TrailS‘𝑔)𝑝𝑓:(0..^(#‘𝑓))–onto→dom (iEdg‘𝑔))
2221, 4, 6copab 4632 . . 3 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(TrailS‘𝑔)𝑝𝑓:(0..^(#‘𝑓))–onto→dom (iEdg‘𝑔))}
232, 3, 22cmpt 4633 . 2 class (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(TrailS‘𝑔)𝑝𝑓:(0..^(#‘𝑓))–onto→dom (iEdg‘𝑔))})
241, 23wceq 1474 1 wff EulerPaths = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(TrailS‘𝑔)𝑝𝑓:(0..^(#‘𝑓))–onto→dom (iEdg‘𝑔))})
Colors of variables: wff setvar class
This definition is referenced by:  releupth  41364  eupths  41365
  Copyright terms: Public domain W3C validator