Metamath Proof Explorer

Theorem eulerpath

Description: A pseudograph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 26-Feb-2021)

Ref Expression
Hypothesis eulerpathpr.v ⊢ V = Vtx ⁡ G
Assertion eulerpath ⊢ G ∈ UPGraph ∧ EulerPaths ⁡ G ≠ ∅ → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ 0 2

Proof

Step Hyp Ref Expression
1 eulerpathpr.v ⊢ V = Vtx ⁡ G
2 releupth ⊢ Rel ⁡ EulerPaths ⁡ G
3 reldm0 ⊢ Rel ⁡ EulerPaths ⁡ G → EulerPaths ⁡ G = ∅ ↔ dom ⁡ EulerPaths ⁡ G = ∅
4 2 3 ax-mp ⊢ EulerPaths ⁡ G = ∅ ↔ dom ⁡ EulerPaths ⁡ G = ∅
5 4 necon3bii ⊢ EulerPaths ⁡ G ≠ ∅ ↔ dom ⁡ EulerPaths ⁡ G ≠ ∅
6 n0 ⊢ dom ⁡ EulerPaths ⁡ G ≠ ∅ ↔ ∃ f f ∈ dom ⁡ EulerPaths ⁡ G
7 5 6 bitri ⊢ EulerPaths ⁡ G ≠ ∅ ↔ ∃ f f ∈ dom ⁡ EulerPaths ⁡ G
8 vex ⊢ f ∈ V
9 8 eldm ⊢ f ∈ dom ⁡ EulerPaths ⁡ G ↔ ∃ p f EulerPaths ⁡ G p
10 1 eulerpathpr ⊢ G ∈ UPGraph ∧ f EulerPaths ⁡ G p → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ 0 2
11 10 expcom ⊢ f EulerPaths ⁡ G p → G ∈ UPGraph → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ 0 2
12 11 exlimiv ⊢ ∃ p f EulerPaths ⁡ G p → G ∈ UPGraph → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ 0 2
13 9 12 sylbi ⊢ f ∈ dom ⁡ EulerPaths ⁡ G → G ∈ UPGraph → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ 0 2
14 13 exlimiv ⊢ ∃ f f ∈ dom ⁡ EulerPaths ⁡ G → G ∈ UPGraph → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ 0 2
15 7 14 sylbi ⊢ EulerPaths ⁡ G ≠ ∅ → G ∈ UPGraph → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ 0 2
16 15 impcom ⊢ G ∈ UPGraph ∧ EulerPaths ⁡ G ≠ ∅ → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ 0 2