Metamath Proof Explorer

Theorem eupths

Description: The Eulerian paths on the graph G . (Contributed by AV, 18-Feb-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Hypothesis eupths.i ⊢ I = iEdg ⁡ G
Assertion eupths ⊢ EulerPaths ⁡ G = f p | f Trails ⁡ G p ∧ f : 0 ..^ f ⟶ onto dom ⁡ I

Proof

Step Hyp Ref Expression
1 eupths.i ⊢ I = iEdg ⁡ G
2 fveq2 ⊢ g = G → iEdg ⁡ g = iEdg ⁡ G
3 2 1 eqtr4di ⊢ g = G → iEdg ⁡ g = I
4 3 dmeqd ⊢ g = G → dom ⁡ iEdg ⁡ g = dom ⁡ I
5 foeq3 ⊢ dom ⁡ iEdg ⁡ g = dom ⁡ I → f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g ↔ f : 0 ..^ f ⟶ onto dom ⁡ I
6 4 5 syl ⊢ g = G → f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g ↔ f : 0 ..^ f ⟶ onto dom ⁡ I
7 df-eupth ⊢ EulerPaths = g ∈ V ⟼ f p | f Trails ⁡ g p ∧ f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g
8 6 7 fvmptopab ⊢ EulerPaths ⁡ G = f p | f Trails ⁡ G p ∧ f : 0 ..^ f ⟶ onto dom ⁡ I