Metamath Proof Explorer


Theorem eupthpf

Description: The P function in an Eulerian path is a function from a finite sequence of nonnegative integers to the vertices. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021)

Ref Expression
Assertion eupthpf
|- ( F ( EulerPaths ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )

Proof

Step Hyp Ref Expression
1 eupthiswlk
 |-  ( F ( EulerPaths ` G ) P -> F ( Walks ` G ) P )
2 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 wlkp
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
4 1 3 syl
 |-  ( F ( EulerPaths ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )