Metamath Proof Explorer

Theorem wspthnonfi

Description: In a finite graph, the set of simple paths of a fixed length between two vertices is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018) (Revised by AV, 15-May-2021)

Ref Expression
Assertion wspthnonfi ⊢ Vtx ⁡ G ∈ Fin → A N WSPathsNOn G B ∈ Fin

Proof

Step Hyp Ref Expression
1 wwlksnonfi ⊢ Vtx ⁡ G ∈ Fin → A N WWalksNOn G B ∈ Fin
2 wspthsswwlknon ⊢ A N WSPathsNOn G B ⊆ A N WWalksNOn G B
3 2 a1i ⊢ Vtx ⁡ G ∈ Fin → A N WSPathsNOn G B ⊆ A N WWalksNOn G B
4 1 3 ssfid ⊢ Vtx ⁡ G ∈ Fin → A N WSPathsNOn G B ∈ Fin