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 | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
Assertion | wlkpwrd | ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 ∈ Word 𝑉 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wlkp.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
2 | 1 | wlkp | ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) |
3 | ffz0iswrd | ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → 𝑃 ∈ Word 𝑉 ) | |
4 | 2 3 | syl | ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 ∈ Word 𝑉 ) |