Theorem clwwlknbp

Description: Basic properties of a closed walk of a fixed length as word. (Contributed by AV, 30-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

	Ref	Expression
Hypothesis	clwwlknwrd.v	|- V = ( Vtx ` G )
Assertion	clwwlknbp	|- ( W e. ( N ClWWalksN G ) -> ( W e. Word V /\ ( # ` W ) = N ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlknwrd.v	|- V = ( Vtx ` G )
2	1	clwwlknwrd	|- ( W e. ( N ClWWalksN G ) -> W e. Word V )
3		clwwlknlen	|- ( W e. ( N ClWWalksN G ) -> ( # ` W ) = N )
4	2 3	jca	|- ( W e. ( N ClWWalksN G ) -> ( W e. Word V /\ ( # ` W ) = N ) )