Metamath Proof Explorer

Theorem wlkpwrd

Description: The sequence of vertices of a walk is a word over the set of vertices. (Contributed by AV, 27-Jan-2021)

Ref Expression
Hypothesis wlkp.v 
|- V = ( Vtx ` G )
Assertion wlkpwrd 
|- ( F ( Walks ` G ) P -> P e. Word V )

Proof

Step Hyp Ref Expression
1 wlkp.v 
 |-  V = ( Vtx ` G )
2 1 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
3 ffz0iswrd 
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> P e. Word V )
4 2 3 syl 
 |-  ( F ( Walks ` G ) P -> P e. Word V )