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

Metamath Proof Explorer

Theorem eupthfi

Description: Any graph with an Eulerian path is of finite size, i.e. with a finite number of edges. (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 18-Feb-2021)

Ref Expression
Hypothesis eupths.i 
|- I = ( iEdg ` G )
Assertion eupthfi 
|- ( F ( EulerPaths ` G ) P -> dom I e. Fin )

Proof

Step Hyp Ref Expression
1 eupths.i 
 |-  I = ( iEdg ` G )
2 fzofi 
 |-  ( 0 ..^ ( # ` F ) ) e. Fin
3 1 eupthf1o 
 |-  ( F ( EulerPaths ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I )
4 ovex 
 |-  ( 0 ..^ ( # ` F ) ) e. _V
5 4 f1oen 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I -> ( 0 ..^ ( # ` F ) ) ~~ dom I )
6 ensym 
 |-  ( ( 0 ..^ ( # ` F ) ) ~~ dom I -> dom I ~~ ( 0 ..^ ( # ` F ) ) )
7 3 5 6 3syl 
 |-  ( F ( EulerPaths ` G ) P -> dom I ~~ ( 0 ..^ ( # ` F ) ) )
8 enfii 
 |-  ( ( ( 0 ..^ ( # ` F ) ) e. Fin /\ dom I ~~ ( 0 ..^ ( # ` F ) ) ) -> dom I e. Fin )
9 2 7 8 sylancr 
 |-  ( F ( EulerPaths ` G ) P -> dom I e. Fin )