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 e. ( N ClWWalksN G ) -> W e. Word V )

Proof

Step	Hyp	Ref	Expression
1		clwwlknwrd.v	|- V = ( Vtx ` G )
2		isclwwlkn	|- ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) )
3	1	clwwlkbp	|- ( W e. ( ClWWalks ` G ) -> ( G e. _V /\ W e. Word V /\ W =/= (/) ) )
4	3	simp2d	|- ( W e. ( ClWWalks ` G ) -> W e. Word V )
5	4	adantr	|- ( ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) -> W e. Word V )
6	2 5	sylbi	|- ( W e. ( N ClWWalksN G ) -> W e. Word V )