Metamath Proof Explorer


Theorem wlklenvp1

Description: The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018) (Revised by AV, 1-May-2021)

Ref Expression
Assertion wlklenvp1
|- ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) )

Proof

Step Hyp Ref Expression
1 wlkcl
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
2 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 wlkp
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
4 ffz0hash
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( # ` P ) = ( ( # ` F ) + 1 ) )
5 1 3 4 syl2anc
 |-  ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) )