Metamath Proof Explorer


Theorem wlksnfi

Description: The number of walks of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 20-Apr-2021)

Ref Expression
Assertion wlksnfi ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0 ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ∈ Fin )

Proof

Step Hyp Ref Expression
1 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 fusgrvtxfi ( 𝐺 ∈ FinUSGraph → ( Vtx ‘ 𝐺 ) ∈ Fin )
3 2 adantr ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0 ) → ( Vtx ‘ 𝐺 ) ∈ Fin )
4 wwlksnfi ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )
5 3 4 syl ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )
6 fusgrusgr ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
7 usgruspgr ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
8 6 7 syl ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USPGraph )
9 wlknwwlksnen ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) )
10 8 9 sylan ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0 ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) )
11 enfii ( ( ( 𝑁 WWalksN 𝐺 ) ∈ Fin ∧ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ≈ ( 𝑁 WWalksN 𝐺 ) ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ∈ Fin )
12 5 10 11 syl2anc ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0 ) → { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ∈ Fin )