Metamath Proof Explorer

Theorem wwlksnfi

Description: The number of walks represented by words of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 30-Jul-2018) (Revised by AV, 19-Apr-2021) (Proof shortened by JJ, 18-Nov-2022)

Ref Expression
Assertion wwlksnfi 
|- ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin )

Proof

Step Hyp Ref Expression
1 wrdnfi 
 |-  ( ( Vtx ` G ) e. Fin -> { w e. Word ( Vtx ` G ) | ( # ` w ) = ( N + 1 ) } e. Fin )
2 simpr 
 |-  ( ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) -> ( # ` w ) = ( N + 1 ) )
3 2 a1i 
 |-  ( w e. Word ( Vtx ` G ) -> ( ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) -> ( # ` w ) = ( N + 1 ) ) )
4 3 ss2rabi 
 |-  { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } C_ { w e. Word ( Vtx ` G ) | ( # ` w ) = ( N + 1 ) }
5 4 a1i 
 |-  ( ( Vtx ` G ) e. Fin -> { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } C_ { w e. Word ( Vtx ` G ) | ( # ` w ) = ( N + 1 ) } )
6 1 5 ssfid 
 |-  ( ( Vtx ` G ) e. Fin -> { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } e. Fin )
7 wwlksn 
 |-  ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )
8 df-rab 
 |-  { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } = { w | ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) }
9 7 8 eqtrdi 
 |-  ( N e. NN0 -> ( N WWalksN G ) = { w | ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) } )
10 3anan12 
 |-  ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( w e. Word ( Vtx ` G ) /\ ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
11 10 anbi1i 
 |-  ( ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) <-> ( ( w e. Word ( Vtx ` G ) /\ ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ ( # ` w ) = ( N + 1 ) ) )
12 anass 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) /\ ( # ` w ) = ( N + 1 ) ) <-> ( w e. Word ( Vtx ` G ) /\ ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) ) )
13 11 12 bitri 
 |-  ( ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) <-> ( w e. Word ( Vtx ` G ) /\ ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) ) )
14 13 abbii 
 |-  { w | ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } = { w | ( w e. Word ( Vtx ` G ) /\ ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) ) }
15 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
16 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
17 15 16 iswwlks 
 |-  ( w e. ( WWalks ` G ) <-> ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
18 17 anbi1i 
 |-  ( ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) <-> ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) )
19 18 abbii 
 |-  { w | ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) } = { w | ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) }
20 df-rab 
 |-  { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } = { w | ( w e. Word ( Vtx ` G ) /\ ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) ) }
21 14 19 20 3eqtr4i 
 |-  { w | ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) } = { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) }
22 9 21 eqtrdi 
 |-  ( N e. NN0 -> ( N WWalksN G ) = { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } )
23 22 eleq1d 
 |-  ( N e. NN0 -> ( ( N WWalksN G ) e. Fin <-> { w e. Word ( Vtx ` G ) | ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = ( N + 1 ) ) } e. Fin ) )
24 6 23 imbitrrid 
 |-  ( N e. NN0 -> ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin ) )
25 df-nel 
 |-  ( N e/ NN0 <-> -. N e. NN0 )
26 25 biimpri 
 |-  ( -. N e. NN0 -> N e/ NN0 )
27 26 olcd 
 |-  ( -. N e. NN0 -> ( G e/ _V \/ N e/ NN0 ) )
28 wwlksnndef 
 |-  ( ( G e/ _V \/ N e/ NN0 ) -> ( N WWalksN G ) = (/) )
29 27 28 syl 
 |-  ( -. N e. NN0 -> ( N WWalksN G ) = (/) )
30 0fi 
 |-  (/) e. Fin
31 29 30 eqeltrdi 
 |-  ( -. N e. NN0 -> ( N WWalksN G ) e. Fin )
32 31 a1d 
 |-  ( -. N e. NN0 -> ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin ) )
33 24 32 pm2.61i 
 |-  ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin )