Metamath Proof Explorer


Theorem wspthsswwlkn

Description: The set of simple paths of a fixed length between two vertices is a subset of the set of walks of the fixed length. (Contributed by AV, 18-May-2021)

Ref Expression
Assertion wspthsswwlkn
|- ( N WSPathsN G ) C_ ( N WWalksN G )

Proof

Step Hyp Ref Expression
1 wspthnp
 |-  ( w e. ( N WSPathsN G ) -> ( ( N e. NN0 /\ G e. _V ) /\ w e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) w ) )
2 1 simp2d
 |-  ( w e. ( N WSPathsN G ) -> w e. ( N WWalksN G ) )
3 2 ssriv
 |-  ( N WSPathsN G ) C_ ( N WWalksN G )