Metamath Proof Explorer

Theorem wlksnfi

Description: The number of walks of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 20-Apr-2021)

Ref Expression
Assertion wlksnfi ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ 0 → p ∈ Walks ⁡ G | 1 st ⁡ p = N ∈ Fin

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 fusgrvtxfi ⊢ G ∈ FinUSGraph → Vtx ⁡ G ∈ Fin
3 2 adantr ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ 0 → Vtx ⁡ G ∈ Fin
4 wwlksnfi ⊢ Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin
5 3 4 syl ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ 0 → N WWalksN G ∈ Fin
6 fusgrusgr ⊢ G ∈ FinUSGraph → G ∈ USGraph
7 usgruspgr ⊢ G ∈ USGraph → G ∈ USHGraph
8 6 7 syl ⊢ G ∈ FinUSGraph → G ∈ USHGraph
9 wlknwwlksnen ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → p ∈ Walks ⁡ G | 1 st ⁡ p = N ≈ N WWalksN G
10 8 9 sylan ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ 0 → p ∈ Walks ⁡ G | 1 st ⁡ p = N ≈ N WWalksN G
11 enfii ⊢ N WWalksN G ∈ Fin ∧ p ∈ Walks ⁡ G | 1 st ⁡ p = N ≈ N WWalksN G → p ∈ Walks ⁡ G | 1 st ⁡ p = N ∈ Fin
12 5 10 11 syl2anc ⊢ G ∈ FinUSGraph ∧ N ∈ ℕ 0 → p ∈ Walks ⁡ G | 1 st ⁡ p = N ∈ Fin