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 rgenw 
 |-  A. 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 ss2rab 
 |-  ( { 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 ) } <-> A. 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 ) ) )
5 3 4 mpbir 
 |-  { 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 5 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 ) } )
7 1 6 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 )
8 wwlksn 
 |-  ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )
9 df-rab 
 |-  { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } = { w | ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) }
10 8 9 eqtrdi 
 |-  ( N e. NN0 -> ( N WWalksN G ) = { w | ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( N + 1 ) ) } )
11 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 ) ) ) )
12 11 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 ) ) )
13 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 ) ) ) )
14 12 13 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 ) ) ) )
15 14 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 ) ) ) }
16 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
17 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
18 16 17 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 ) ) )
19 18 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 ) ) )
20 19 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 ) ) }
21 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 ) ) ) }
22 15 20 21 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 ) ) }
23 10 22 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 ) ) } )
24 23 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 ) )
25 7 24 syl5ibr 
 |-  ( N e. NN0 -> ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin ) )
26 df-nel 
 |-  ( N e/ NN0 <-> -. N e. NN0 )
27 26 biimpri 
 |-  ( -. N e. NN0 -> N e/ NN0 )
28 27 olcd 
 |-  ( -. N e. NN0 -> ( G e/ _V \/ N e/ NN0 ) )
29 wwlksnndef 
 |-  ( ( G e/ _V \/ N e/ NN0 ) -> ( N WWalksN G ) = (/) )
30 28 29 syl 
 |-  ( -. N e. NN0 -> ( N WWalksN G ) = (/) )
31 0fin 
 |-  (/) e. Fin
32 30 31 eqeltrdi 
 |-  ( -. N e. NN0 -> ( N WWalksN G ) e. Fin )
33 32 a1d 
 |-  ( -. N e. NN0 -> ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin ) )
34 25 33 pm2.61i 
 |-  ( ( Vtx ` G ) e. Fin -> ( N WWalksN G ) e. Fin )