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