Metamath Proof Explorer

Theorem clwwlknwrd

Description: A closed walk of a fixed length as word is a word over the vertices. (Contributed by AV, 30-Apr-2021)

		Ref	Expression
	Hypothesis	clwwlknwrd.v	$⊢ V = Vtx (G)$
	Assertion	clwwlknwrd	$⊢ W \in (N ClWWalksN G) \to W \in Word V$

Step	Hyp	Ref	Expression
1		clwwlknwrd.v	$⊢ V = Vtx (G)$
2		isclwwlkn	$⊢ W \in (N ClWWalksN G) \leftrightarrow (W \in ClWWalks (G) \land \|W\| = N)$
3	1	clwwlkbp	$⊢ W \in ClWWalks (G) \to (G \in V \land W \in Word V \land W \neq \emptyset)$
4	3	simp2d	$⊢ W \in ClWWalks (G) \to W \in Word V$
5	4	adantr	$⊢ (W \in ClWWalks (G) \land \|W\| = N) \to W \in Word V$
6	2 5	sylbi	$⊢ W \in (N ClWWalksN G) \to W \in Word V$