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 ) |
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 ) |