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

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 
|- ( ( 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 )