Metamath Proof Explorer

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 ` G ) C_ Word ( Vtx ` G )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 clwwlk 
 |-  ( ClWWalks ` G ) = { w e. Word ( Vtx ` G ) | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` w ) , ( w ` 0 ) } e. ( Edg ` G ) ) }
4 3 ssrab3 
 |-  ( ClWWalks ` G ) C_ Word ( Vtx ` G )