This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \to P \in Word V$

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