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 e. UPGraph /\ ( EulerPaths ` G ) =/= (/) ) -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 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 ) =/= (/) <-> E. f f e. dom ( EulerPaths ` G ) )
7 5 6 bitri 
 |-  ( ( EulerPaths ` G ) =/= (/) <-> E. f f e. dom ( EulerPaths ` G ) )
8 vex 
 |-  f e. _V
9 8 eldm 
 |-  ( f e. dom ( EulerPaths ` G ) <-> E. p f ( EulerPaths ` G ) p )
10 1 eulerpathpr 
 |-  ( ( G e. UPGraph /\ f ( EulerPaths ` G ) p ) -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } )
11 10 expcom 
 |-  ( f ( EulerPaths ` G ) p -> ( G e. UPGraph -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } ) )
12 11 exlimiv 
 |-  ( E. p f ( EulerPaths ` G ) p -> ( G e. UPGraph -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } ) )
13 9 12 sylbi 
 |-  ( f e. dom ( EulerPaths ` G ) -> ( G e. UPGraph -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } ) )
14 13 exlimiv 
 |-  ( E. f f e. dom ( EulerPaths ` G ) -> ( G e. UPGraph -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } ) )
15 7 14 sylbi 
 |-  ( ( EulerPaths ` G ) =/= (/) -> ( G e. UPGraph -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } ) )
16 15 impcom 
 |-  ( ( G e. UPGraph /\ ( EulerPaths ` G ) =/= (/) ) -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } )