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 |
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 |