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\mathrm{WSPathsN}G\subseteq N\mathrm{WWalksN}G$$

Proof

Step	Hyp	Ref	Expression
1		wspthnp	$$⊢w\in \left(N\mathrm{WSPathsN}G\right)\to \left(\left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\wedge w\in \left(N\mathrm{WWalksN}G\right)\wedge \exists ff\mathrm{SPaths}\left(G\right)w\right)$$
2	1	simp2d	$$⊢w\in \left(N\mathrm{WSPathsN}G\right)\to w\in \left(N\mathrm{WWalksN}G\right)$$
3	2	ssriv	$$⊢N\mathrm{WSPathsN}G\subseteq N\mathrm{WWalksN}G$$