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