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	⊢ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ⊆ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2	1	wspthnonp	⊢ ( 𝑤 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
3		simp3l	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) → 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) )
4	2 3	syl	⊢ ( 𝑤 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) → 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) )
5	4	ssriv	⊢ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ⊆ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 )