Metamath Proof Explorer

Theorem clwwlknfi

Description: If there is only a finite number of vertices, the number of closed walks of fixed length (as words) is also finite. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 25-Apr-2021) (Proof shortened by AV, 22-Mar-2022) (Proof shortened by JJ, 18-Nov-2022)

Ref Expression
Assertion clwwlknfi ⊢ Vtx ⁡ G ∈ Fin → N ClWWalksN G ∈ Fin

Proof

Step Hyp Ref Expression
1 clwwlkn ⊢ N ClWWalksN G = w ∈ ClWWalks ⁡ G | w = N
2 wrdnfi ⊢ Vtx ⁡ G ∈ Fin → w ∈ Word Vtx ⁡ G | w = N ∈ Fin
3 clwwlksswrd ⊢ ClWWalks ⁡ G ⊆ Word Vtx ⁡ G
4 rabss2 ⊢ ClWWalks ⁡ G ⊆ Word Vtx ⁡ G → w ∈ ClWWalks ⁡ G | w = N ⊆ w ∈ Word Vtx ⁡ G | w = N
5 3 4 mp1i ⊢ Vtx ⁡ G ∈ Fin → w ∈ ClWWalks ⁡ G | w = N ⊆ w ∈ Word Vtx ⁡ G | w = N
6 2 5 ssfid ⊢ Vtx ⁡ G ∈ Fin → w ∈ ClWWalks ⁡ G | w = N ∈ Fin
7 1 6 eqeltrid ⊢ Vtx ⁡ G ∈ Fin → N ClWWalksN G ∈ Fin