This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Walks, paths and cycles Walks as words 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