Metamath Proof Explorer

Theorem clwwlknonfin

Description: In a finite graph G , the set of closed walks on vertex X of length N is also finite. (Contributed by Alexander van der Vekens, 26-Sep-2018) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 24-Mar-2022)

Ref Expression
Hypothesis clwwlknonfin.v ⊢ V = Vtx ⁡ G
Assertion clwwlknonfin ⊢ V ∈ Fin → X ClWWalksNOn ⁡ G N ∈ Fin

Proof

Step Hyp Ref Expression
1 clwwlknonfin.v ⊢ V = Vtx ⁡ G
2 clwwlknon ⊢ X ClWWalksNOn ⁡ G N = w ∈ N ClWWalksN G | w ⁡ 0 = X
3 1 eleq1i ⊢ V ∈ Fin ↔ Vtx ⁡ G ∈ Fin
4 clwwlknfi ⊢ Vtx ⁡ G ∈ Fin → N ClWWalksN G ∈ Fin
5 3 4 sylbi ⊢ V ∈ Fin → N ClWWalksN G ∈ Fin
6 rabfi ⊢ N ClWWalksN G ∈ Fin → w ∈ N ClWWalksN G | w ⁡ 0 = X ∈ Fin
7 5 6 syl ⊢ V ∈ Fin → w ∈ N ClWWalksN G | w ⁡ 0 = X ∈ Fin
8 2 7 eqeltrid ⊢ V ∈ Fin → X ClWWalksNOn ⁡ G N ∈ Fin