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

Definition df-eupa 26490
 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 26489 . 2 class EulPaths
2 vv . . 3 setvar 𝑣
3 ve . . 3 setvar 𝑒
4 cvv 3173 . . 3 class V
52cv 1474 . . . . . 6 class 𝑣
63cv 1474 . . . . . 6 class 𝑒
7 cumg 25841 . . . . . 6 class UMGrph
85, 6, 7wbr 4583 . . . . 5 wff 𝑣 UMGrph 𝑒
9 c1 9816 . . . . . . . . 9 class 1
10 vn . . . . . . . . . 10 setvar 𝑛
1110cv 1474 . . . . . . . . 9 class 𝑛
12 cfz 12197 . . . . . . . . 9 class ...
139, 11, 12co 6549 . . . . . . . 8 class (1...𝑛)
146cdm 5038 . . . . . . . 8 class dom 𝑒
15 vf . . . . . . . . 9 setvar 𝑓
1615cv 1474 . . . . . . . 8 class 𝑓
1713, 14, 16wf1o 5803 . . . . . . 7 wff 𝑓:(1...𝑛)–1-1-onto→dom 𝑒
18 cc0 9815 . . . . . . . . 9 class 0
1918, 11, 12co 6549 . . . . . . . 8 class (0...𝑛)
20 vp . . . . . . . . 9 setvar 𝑝
2120cv 1474 . . . . . . . 8 class 𝑝
2219, 5, 21wf 5800 . . . . . . 7 wff 𝑝:(0...𝑛)⟶𝑣
23 vk . . . . . . . . . . . 12 setvar 𝑘
2423cv 1474 . . . . . . . . . . 11 class 𝑘
2524, 16cfv 5804 . . . . . . . . . 10 class (𝑓𝑘)
2625, 6cfv 5804 . . . . . . . . 9 class (𝑒‘(𝑓𝑘))
27 cmin 10145 . . . . . . . . . . . 12 class
2824, 9, 27co 6549 . . . . . . . . . . 11 class (𝑘 − 1)
2928, 21cfv 5804 . . . . . . . . . 10 class (𝑝‘(𝑘 − 1))
3024, 21cfv 5804 . . . . . . . . . 10 class (𝑝𝑘)
3129, 30cpr 4127 . . . . . . . . 9 class {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}
3226, 31wceq 1475 . . . . . . . 8 wff (𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}
3332, 23, 13wral 2896 . . . . . . 7 wff 𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}
3417, 22, 33w3a 1031 . . . . . 6 wff (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})
35 cn0 11169 . . . . . 6 class 0
3634, 10, 35wrex 2897 . . . . 5 wff 𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})
378, 36wa 383 . . . 4 wff (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))
3837, 15, 20copab 4642 . . 3 class {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))}
392, 3, 4, 4, 38cmpt2 6551 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))})
401, 39wceq 1475 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  26491  iseupa  26492  eupatrl  26495
 Copyright terms: Public domain W3C validator