This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Walks, paths and cycles Walks as words 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 ⊢ ( 𝑁 WSPathsN 𝐺 ) ⊆ ( 𝑁 WWalksN 𝐺 )
Proof
Step
Hyp
Ref
Expression
1
wspthnp ⊢ ( 𝑤 ∈ ( 𝑁 WSPathsN 𝐺 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
2
1
simp2d ⊢ ( 𝑤 ∈ ( 𝑁 WSPathsN 𝐺 ) → 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) )
3
2
ssriv ⊢ ( 𝑁 WSPathsN 𝐺 ) ⊆ ( 𝑁 WWalksN 𝐺 )