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