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 )