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=\mathrm{Vtx}\left(G\right)$$
Assertion	wlkpwrd	$$⊢F\mathrm{Walks}\left(G\right)P\to P\in \mathrm{Word}V$$

Proof

Step	Hyp	Ref	Expression
1		wlkp.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	wlkp	$$⊢F\mathrm{Walks}\left(G\right)P\to P:\left(0\dots \left|F\right|\right)⟶V$$
3		ffz0iswrd	$$⊢P:\left(0\dots \left|F\right|\right)⟶V\to P\in \mathrm{Word}V$$
4	2 3	syl	$$⊢F\mathrm{Walks}\left(G\right)P\to P\in \mathrm{Word}V$$