This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion eulerpath ( ( 𝐺 ∈ UPGraph ∧ ( EulerPaths ‘ 𝐺 ) ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } )

Proof

Step Hyp Ref Expression
1 eulerpathpr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 releupth ⊢ Rel ( EulerPaths ‘ 𝐺 )
3 reldm0 ⊢ ( Rel ( EulerPaths ‘ 𝐺 ) → ( ( EulerPaths ‘ 𝐺 ) = ∅ ↔ dom ( EulerPaths ‘ 𝐺 ) = ∅ ) )
4 2 3 ax-mp ⊢ ( ( EulerPaths ‘ 𝐺 ) = ∅ ↔ dom ( EulerPaths ‘ 𝐺 ) = ∅ )
5 4 necon3bii ⊢ ( ( EulerPaths ‘ 𝐺 ) ≠ ∅ ↔ dom ( EulerPaths ‘ 𝐺 ) ≠ ∅ )
6 n0 ⊢ ( dom ( EulerPaths ‘ 𝐺 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ dom ( EulerPaths ‘ 𝐺 ) )
7 5 6 bitri ⊢ ( ( EulerPaths ‘ 𝐺 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ dom ( EulerPaths ‘ 𝐺 ) )
8 vex ⊢ 𝑓 ∈ V
9 8 eldm ⊢ ( 𝑓 ∈ dom ( EulerPaths ‘ 𝐺 ) ↔ ∃ 𝑝 𝑓 ( EulerPaths ‘ 𝐺 ) 𝑝 )
10 1 eulerpathpr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑓 ( EulerPaths ‘ 𝐺 ) 𝑝 ) → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } )
11 10 expcom ⊢ ( 𝑓 ( EulerPaths ‘ 𝐺 ) 𝑝 → ( 𝐺 ∈ UPGraph → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) )
12 11 exlimiv ⊢ ( ∃ 𝑝 𝑓 ( EulerPaths ‘ 𝐺 ) 𝑝 → ( 𝐺 ∈ UPGraph → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) )
13 9 12 sylbi ⊢ ( 𝑓 ∈ dom ( EulerPaths ‘ 𝐺 ) → ( 𝐺 ∈ UPGraph → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) )
14 13 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ dom ( EulerPaths ‘ 𝐺 ) → ( 𝐺 ∈ UPGraph → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) )
15 7 14 sylbi ⊢ ( ( EulerPaths ‘ 𝐺 ) ≠ ∅ → ( 𝐺 ∈ UPGraph → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) )
16 15 impcom ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( EulerPaths ‘ 𝐺 ) ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } )