Metamath Proof Explorer

Theorem wwlksnonfi

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

Ref Expression
Assertion wwlksnonfi ⊢ Vtx ⁡ G ∈ Fin → A N WWalksNOn G B ∈ Fin

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 iswwlksnon ⊢ A N WWalksNOn G B = w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B
3 wwlksnfi ⊢ Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin
4 rabfi ⊢ N WWalksN G ∈ Fin → w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B ∈ Fin
5 3 4 syl ⊢ Vtx ⁡ G ∈ Fin → w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B ∈ Fin
6 2 5 eqeltrid ⊢ Vtx ⁡ G ∈ Fin → A N WWalksNOn G B ∈ Fin