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 6 adantl ⊢ ⊤ ∧ g = G → f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g ↔ f : 0 ..^ f ⟶ onto dom ⁡ I
8 wksv ⊢ f p | f Walks ⁡ G p ∈ V
9 trliswlk ⊢ f Trails ⁡ G p → f Walks ⁡ G p
10 9 ssopab2i ⊢ f p | f Trails ⁡ G p ⊆ f p | f Walks ⁡ G p
11 8 10 ssexi ⊢ f p | f Trails ⁡ G p ∈ V
12 11 a1i ⊢ ⊤ → f p | f Trails ⁡ G p ∈ V
13 df-eupth ⊢ EulerPaths = g ∈ V ⟼ f p | f Trails ⁡ g p ∧ f : 0 ..^ f ⟶ onto dom ⁡ iEdg ⁡ g
14 7 12 13 fvmptopab ⊢ ⊤ → EulerPaths ⁡ G = f p | f Trails ⁡ G p ∧ f : 0 ..^ f ⟶ onto dom ⁡ I
15 14 mptru ⊢ EulerPaths ⁡ G = f p | f Trails ⁡ G p ∧ f : 0 ..^ f ⟶ onto dom ⁡ I