Theorem clwwlksswrd

Description: Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 25-Apr-2021)

	Ref	Expression
Assertion	clwwlksswrd	⊢ ( ClWWalks ‘ 𝐺 ) ⊆ Word ( Vtx ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3	1 2	clwwlk	⊢ ( ClWWalks ‘ 𝐺 ) = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) }
4	3	ssrab3	⊢ ( ClWWalks ‘ 𝐺 ) ⊆ Word ( Vtx ‘ 𝐺 )