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 } )