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	|- ( ( G e. FinUSGraph /\ N e. NN0 ) -> { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } e. Fin )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
2	1	fusgrvtxfi	|- ( G e. FinUSGraph -> ( Vtx ` G ) e. Fin )
3	2	adantr	|- ( ( G e. FinUSGraph /\ N e. NN0 ) -> ( Vtx ` G ) e. Fin )
4		wwlksnfi	|- ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin )
5	3 4	syl	|- ( ( G e. FinUSGraph /\ N e. NN0 ) -> ( N WWalksN G ) e. Fin )
6		fusgrusgr	|- ( G e. FinUSGraph -> G e. USGraph )
7		usgruspgr	|- ( G e. USGraph -> G e. USPGraph )
8	6 7	syl	|- ( G e. FinUSGraph -> G e. USPGraph )
9		wlknwwlksnen	|- ( ( G e. USPGraph /\ N e. NN0 ) -> { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ~~ ( N WWalksN G ) )
10	8 9	sylan	|- ( ( G e. FinUSGraph /\ N e. NN0 ) -> { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ~~ ( N WWalksN G ) )
11		enfii	|- ( ( ( N WWalksN G ) e. Fin /\ { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ~~ ( N WWalksN G ) ) -> { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } e. Fin )
12	5 10 11	syl2anc	|- ( ( G e. FinUSGraph /\ N e. NN0 ) -> { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } e. Fin )