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 \subseteq A (N WWalksNOn G) B$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2	1	wspthnonp	$⊢ w \in (A (N WSPathsNOn G) B) \to ((N \in ℕ_{0} \land G \in V) \land (A \in Vtx (G) \land B \in Vtx (G)) \land (w \in (A (N WWalksNOn G) B) \land \exists f f (A SPathsOn (G) B) w))$
3		simp3l	$⊢ ((N \in ℕ_{0} \land G \in V) \land (A \in Vtx (G) \land B \in Vtx (G)) \land (w \in (A (N WWalksNOn G) B) \land \exists f f (A SPathsOn (G) B) w)) \to w \in (A (N WWalksNOn G) B)$
4	2 3	syl	$⊢ w \in (A (N WSPathsNOn G) B) \to w \in (A (N WWalksNOn G) B)$
5	4	ssriv	$⊢ A (N WSPathsNOn G) B \subseteq A (N WWalksNOn G) B$