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

Definition df-eupa 26256
Description: Define the set of all Eulerian paths on an undirected multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.)
Assertion
Ref Expression
df-eupa EulPaths = (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))})
Distinct variable group:   𝑒,𝑓,𝑘,𝑛,𝑝,𝑣

Detailed syntax breakdown of Definition df-eupa
StepHypRef Expression
1 ceup 26255 . 2 class EulPaths
2 vv . . 3 setvar 𝑣
3 ve . . 3 setvar 𝑒
4 cvv 3172 . . 3 class V
52cv 1473 . . . . . 6 class 𝑣
63cv 1473 . . . . . 6 class 𝑒
7 cumg 25607 . . . . . 6 class UMGrph
85, 6, 7wbr 4577 . . . . 5 wff 𝑣 UMGrph 𝑒
9 c1 9793 . . . . . . . . 9 class 1
10 vn . . . . . . . . . 10 setvar 𝑛
1110cv 1473 . . . . . . . . 9 class 𝑛
12 cfz 12152 . . . . . . . . 9 class ...
139, 11, 12co 6527 . . . . . . . 8 class (1...𝑛)
146cdm 5028 . . . . . . . 8 class dom 𝑒
15 vf . . . . . . . . 9 setvar 𝑓
1615cv 1473 . . . . . . . 8 class 𝑓
1713, 14, 16wf1o 5789 . . . . . . 7 wff 𝑓:(1...𝑛)–1-1-onto→dom 𝑒
18 cc0 9792 . . . . . . . . 9 class 0
1918, 11, 12co 6527 . . . . . . . 8 class (0...𝑛)
20 vp . . . . . . . . 9 setvar 𝑝
2120cv 1473 . . . . . . . 8 class 𝑝
2219, 5, 21wf 5786 . . . . . . 7 wff 𝑝:(0...𝑛)⟶𝑣
23 vk . . . . . . . . . . . 12 setvar 𝑘
2423cv 1473 . . . . . . . . . . 11 class 𝑘
2524, 16cfv 5790 . . . . . . . . . 10 class (𝑓𝑘)
2625, 6cfv 5790 . . . . . . . . 9 class (𝑒‘(𝑓𝑘))
27 cmin 10117 . . . . . . . . . . . 12 class
2824, 9, 27co 6527 . . . . . . . . . . 11 class (𝑘 − 1)
2928, 21cfv 5790 . . . . . . . . . 10 class (𝑝‘(𝑘 − 1))
3024, 21cfv 5790 . . . . . . . . . 10 class (𝑝𝑘)
3129, 30cpr 4126 . . . . . . . . 9 class {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}
3226, 31wceq 1474 . . . . . . . 8 wff (𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}
3332, 23, 13wral 2895 . . . . . . 7 wff 𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}
3417, 22, 33w3a 1030 . . . . . 6 wff (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})
35 cn0 11139 . . . . . 6 class 0
3634, 10, 35wrex 2896 . . . . 5 wff 𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})
378, 36wa 382 . . . 4 wff (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))
3837, 15, 20copab 4636 . . 3 class {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))}
392, 3, 4, 4, 38cmpt2 6529 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))})
401, 39wceq 1474 1 wff EulPaths = (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))})
Colors of variables: wff setvar class
This definition is referenced by:  releupa  26257  iseupa  26258  eupatrl  26261
  Copyright terms: Public domain W3C validator