Metamath Proof Explorer


Theorem wspthsswwlknon

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 between the two vertices. (Contributed by AV, 15-May-2021)

Ref Expression
Assertion wspthsswwlknon A N WSPathsNOn G B A N WWalksNOn G B

Proof

Step Hyp Ref Expression
1 eqid Vtx G = Vtx G
2 1 wspthnonp w A N WSPathsNOn G B N 0 G V A Vtx G B Vtx G w A N WWalksNOn G B f f A SPathsOn G B w
3 simp3l N 0 G V A Vtx G B Vtx G w A N WWalksNOn G B f f A SPathsOn G B w w A N WWalksNOn G B
4 2 3 syl w A N WSPathsNOn G B w A N WWalksNOn G B
5 4 ssriv A N WSPathsNOn G B A N WWalksNOn G B