This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \subseteq N WWalksN G$

Proof

Step	Hyp	Ref	Expression
1		wspthnp	$⊢ w \in (N WSPathsN G) \to ((N \in ℕ_{0} \land G \in V) \land w \in (N WWalksN G) \land \exists f f SPaths (G) w)$
2	1	simp2d	$⊢ w \in (N WSPathsN G) \to w \in (N WWalksN G)$
3	2	ssriv	$⊢ N WSPathsN G \subseteq N WWalksN G$