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

Metamath Proof Explorer

Theorem 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 (G) \in Fin \to N WSPathsN G \in Fin$

Proof

Step	Hyp	Ref	Expression
1		wwlksnfi	$⊢ Vtx (G) \in Fin \to N WWalksN G \in Fin$
2		wspthsswwlkn	$⊢ N WSPathsN G \subseteq N WWalksN G$
3	2	a1i	$⊢ Vtx (G) \in Fin \to N WSPathsN G \subseteq N WWalksN G$
4	1 3	ssfid	$⊢ Vtx (G) \in Fin \to N WSPathsN G \in Fin$