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 )