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

Step	Hyp	Ref	Expression
1		ceup 26489	. 2 class EulPaths
2		vv	. . 3 setvar 𝑣
3		ve	. . 3 setvar 𝑒
4		cvv 3173	. . 3 class V
5	2	cv 1474	. . . . . 6 class 𝑣
6	3	cv 1474	. . . . . 6 class 𝑒
7		cumg 25841	. . . . . 6 class UMGrph
8	5, 6, 7	wbr 4583	. . . . 5 wff 𝑣 UMGrph 𝑒
9		c1 9816	. . . . . . . . 9 class 1
10		vn	. . . . . . . . . 10 setvar 𝑛
11	10	cv 1474	. . . . . . . . 9 class 𝑛
12		cfz 12197	. . . . . . . . 9 class ...
13	9, 11, 12	co 6549	. . . . . . . 8 class (1...𝑛)
14	6	cdm 5038	. . . . . . . 8 class dom 𝑒
15		vf	. . . . . . . . 9 setvar 𝑓
16	15	cv 1474	. . . . . . . 8 class 𝑓
17	13, 14, 16	wf1o 5803	. . . . . . 7 wff 𝑓:(1...𝑛)–1-1-onto→dom 𝑒
18		cc0 9815	. . . . . . . . 9 class 0
19	18, 11, 12	co 6549	. . . . . . . 8 class (0...𝑛)
20		vp	. . . . . . . . 9 setvar 𝑝
21	20	cv 1474	. . . . . . . 8 class 𝑝
22	19, 5, 21	wf 5800	. . . . . . 7 wff 𝑝:(0...𝑛)⟶𝑣
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1474	. . . . . . . . . . 11 class 𝑘
25	24, 16	cfv 5804	. . . . . . . . . 10 class (𝑓‘𝑘)
26	25, 6	cfv 5804	. . . . . . . . 9 class (𝑒‘(𝑓‘𝑘))
27		cmin 10145	. . . . . . . . . . . 12 class −
28	24, 9, 27	co 6549	. . . . . . . . . . 11 class (𝑘 − 1)
29	28, 21	cfv 5804	. . . . . . . . . 10 class (𝑝‘(𝑘 − 1))
30	24, 21	cfv 5804	. . . . . . . . . 10 class (𝑝‘𝑘)
31	29, 30	cpr 4127	. . . . . . . . 9 class {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}
32	26, 31	wceq 1475	. . . . . . . 8 wff (𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}
33	32, 23, 13	wral 2896	. . . . . . 7 wff ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}
34	17, 22, 33	w3a 1031	. . . . . 6 wff (𝑓:(1...𝑛)–1-1-onto→dom 𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})
35		cn0 11169	. . . . . 6 class ℕ0
36	34, 10, 35	wrex 2897	. . . . 5 wff ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})
37	8, 36	wa 383	. . . 4 wff (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))
38	37, 15, 20	copab 4642	. . 3 class {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))}
39	2, 3, 4, 4, 38	cmpt2 6551	. 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))})
40	1, 39	wceq 1475	1 wff EulPaths = (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))})

This definition is referenced by:  releupa  26491  iseupa  26492  eupatrl  26495