Metamath Proof Explorer


Theorem wwlkssswrd

Description: Walks (represented by words) are words. (Contributed by Alexander van der Vekens, 17-Jul-2018) (Revised by AV, 9-Apr-2021)

Ref Expression
Hypothesis wwlkssswrd.v
|- V = ( Vtx ` G )
Assertion wwlkssswrd
|- ( WWalks ` G ) C_ Word V

Proof

Step Hyp Ref Expression
1 wwlkssswrd.v
 |-  V = ( Vtx ` G )
2 1 wwlkbp
 |-  ( w e. ( WWalks ` G ) -> ( G e. _V /\ w e. Word V ) )
3 2 simprd
 |-  ( w e. ( WWalks ` G ) -> w e. Word V )
4 3 ssriv
 |-  ( WWalks ` G ) C_ Word V