This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐺 ) ∈ Fin → ( 𝑁 ClWWalksN 𝐺 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 clwwlkn ⊢ ( 𝑁 ClWWalksN 𝐺 ) = { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 }
2 wrdnfi ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ∈ Fin )
3 clwwlksswrd ⊢ ( ClWWalks ‘ 𝐺 ) ⊆ Word ( Vtx ‘ 𝐺 )
4 rabss2 ⊢ ( ( ClWWalks ‘ 𝐺 ) ⊆ Word ( Vtx ‘ 𝐺 ) → { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ⊆ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } )
5 3 4 mp1i ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ⊆ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } )
6 2 5 ssfid ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → { 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ∈ Fin )
7 1 6 eqeltrid ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 ClWWalksN 𝐺 ) ∈ Fin )