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∈02

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≠∅↔∃ff∈dom⁡EulerPaths⁡G
7 5 6 bitri ⊢EulerPaths⁡G≠∅↔∃ff∈dom⁡EulerPaths⁡G
8 vex ⊢f∈V
9 8 eldm ⊢f∈dom⁡EulerPaths⁡G↔∃pfEulerPaths⁡Gp
10 1 eulerpathpr ⊢G∈UPGraph∧fEulerPaths⁡Gp→x∈V|¬2∥VtxDeg⁡G⁡x∈02
11 10 expcom ⊢fEulerPaths⁡Gp→G∈UPGraph→x∈V|¬2∥VtxDeg⁡G⁡x∈02
12 11 exlimiv ⊢∃pfEulerPaths⁡Gp→G∈UPGraph→x∈V|¬2∥VtxDeg⁡G⁡x∈02
13 9 12 sylbi ⊢f∈dom⁡EulerPaths⁡G→G∈UPGraph→x∈V|¬2∥VtxDeg⁡G⁡x∈02
14 13 exlimiv ⊢∃ff∈dom⁡EulerPaths⁡G→G∈UPGraph→x∈V|¬2∥VtxDeg⁡G⁡x∈02
15 7 14 sylbi ⊢EulerPaths⁡G≠∅→G∈UPGraph→x∈V|¬2∥VtxDeg⁡G⁡x∈02
16 15 impcom ⊢G∈UPGraph∧EulerPaths⁡G≠∅→x∈V|¬2∥VtxDeg⁡G⁡x∈02