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

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 ( 𝐴 ( 𝑁 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 𝐺 ) 𝐵 )