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 wspthnfi
Description: In a finite graph, the set of simple paths of a fixed length is finite.
(Contributed by Alexander van der Vekens , 4-Mar-2018) (Revised by AV , 18-May-2021)
Ref
Expression
Assertion
wspthnfi ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WSPathsN 𝐺 ) ∈ Fin )
Proof
Step
Hyp
Ref
Expression
1
wwlksnfi ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )
2
wspthsswwlkn ⊢ ( 𝑁 WSPathsN 𝐺 ) ⊆ ( 𝑁 WWalksN 𝐺 )
3
2
a1i ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WSPathsN 𝐺 ) ⊆ ( 𝑁 WWalksN 𝐺 ) )
4
1 3
ssfid ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WSPathsN 𝐺 ) ∈ Fin )