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 ) e. Fin -> ( N ClWWalksN G ) e. Fin )

Proof

Step Hyp Ref Expression
1 clwwlkn 
 |-  ( N ClWWalksN G ) = { w e. ( ClWWalks ` G ) | ( # ` w ) = N }
2 wrdnfi 
 |-  ( ( Vtx ` G ) e. Fin -> { w e. Word ( Vtx ` G ) | ( # ` w ) = N } e. Fin )
3 clwwlksswrd 
 |-  ( ClWWalks ` G ) C_ Word ( Vtx ` G )
4 rabss2 
 |-  ( ( ClWWalks ` G ) C_ Word ( Vtx ` G ) -> { w e. ( ClWWalks ` G ) | ( # ` w ) = N } C_ { w e. Word ( Vtx ` G ) | ( # ` w ) = N } )
5 3 4 mp1i 
 |-  ( ( Vtx ` G ) e. Fin -> { w e. ( ClWWalks ` G ) | ( # ` w ) = N } C_ { w e. Word ( Vtx ` G ) | ( # ` w ) = N } )
6 2 5 ssfid 
 |-  ( ( Vtx ` G ) e. Fin -> { w e. ( ClWWalks ` G ) | ( # ` w ) = N } e. Fin )
7 1 6 eqeltrid 
 |-  ( ( Vtx ` G ) e. Fin -> ( N ClWWalksN G ) e. Fin )