Metamath Proof Explorer

Definition df-eupth

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)

Ref Expression
Assertion df-eupth ⊢ EulerPaths = g ∈ V ⟼ f p | f Trails ⁡ g p ∧ f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g

Detailed syntax breakdown

Step Hyp Ref Expression
0 ceupth class EulerPaths
1 vg setvar g
2 cvv class V
3 vf setvar f
4 vp setvar p
5 3 cv setvar f
6 ctrls class Trails
7 1 cv setvar g
8 7 6 cfv class Trails ⁡ g
9 4 cv setvar p
10 5 9 8 wbr wff f Trails ⁡ g p
11 cc0 class 0
12 cfzo class ..^
13 chash class .
14 5 13 cfv class f
15 11 14 12 co class 0 ..^ f
16 ciedg class iEdg
17 7 16 cfv class iEdg ⁡ g
18 17 cdm class dom ⁡ iEdg ⁡ g
19 15 18 5 wfo wff f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g
20 10 19 wa wff f Trails ⁡ g p ∧ f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g
21 20 3 4 copab class f p | f Trails ⁡ g p ∧ f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g
22 1 2 21 cmpt class g ∈ V ⟼ f p | f Trails ⁡ g p ∧ f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g
23 0 22 wceq wff EulerPaths = g ∈ V ⟼ f p | f Trails ⁡ g p ∧ f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g