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 Fin N WWalksN G Fin

Proof

Step Hyp Ref Expression
1 wrdnfi Vtx G Fin w Word Vtx G | w = N + 1 Fin
2 simpr w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 w = N + 1
3 2 rgenw w Word Vtx G w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 w = N + 1
4 ss2rab w Word Vtx G | w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 w Word Vtx G | w = N + 1 w Word Vtx G w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 w = N + 1
5 3 4 mpbir w Word Vtx G | w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 w Word Vtx G | w = N + 1
6 5 a1i Vtx G Fin w Word Vtx G | w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 w Word Vtx G | w = N + 1
7 1 6 ssfid Vtx G Fin w Word Vtx G | w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 Fin
8 wwlksn N 0 N WWalksN G = w WWalks G | w = N + 1
9 df-rab w WWalks G | w = N + 1 = w | w WWalks G w = N + 1
10 8 9 eqtrdi N 0 N WWalksN G = w | w WWalks G w = N + 1
11 3anan12 w w Word Vtx G i 0 ..^ w 1 w i w i + 1 Edg G w Word Vtx G w i 0 ..^ w 1 w i w i + 1 Edg G
12 11 anbi1i w w Word Vtx G i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 w Word Vtx G w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1
13 anass w Word Vtx G w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 w Word Vtx G w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1
14 12 13 bitri w w Word Vtx G i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 w Word Vtx G w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1
15 14 abbii w | w w Word Vtx G i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 = w | w Word Vtx G w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1
16 eqid Vtx G = Vtx G
17 eqid Edg G = Edg G
18 16 17 iswwlks w WWalks G w w Word Vtx G i 0 ..^ w 1 w i w i + 1 Edg G
19 18 anbi1i w WWalks G w = N + 1 w w Word Vtx G i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1
20 19 abbii w | w WWalks G w = N + 1 = w | w w Word Vtx G i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1
21 df-rab w Word Vtx G | w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 = w | w Word Vtx G w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1
22 15 20 21 3eqtr4i w | w WWalks G w = N + 1 = w Word Vtx G | w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1
23 10 22 eqtrdi N 0 N WWalksN G = w Word Vtx G | w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1
24 23 eleq1d N 0 N WWalksN G Fin w Word Vtx G | w i 0 ..^ w 1 w i w i + 1 Edg G w = N + 1 Fin
25 7 24 syl5ibr N 0 Vtx G Fin N WWalksN G Fin
26 df-nel N 0 ¬ N 0
27 26 biimpri ¬ N 0 N 0
28 27 olcd ¬ N 0 G V N 0
29 wwlksnndef G V N 0 N WWalksN G =
30 28 29 syl ¬ N 0 N WWalksN G =
31 0fin Fin
32 30 31 eqeltrdi ¬ N 0 N WWalksN G Fin
33 32 a1d ¬ N 0 Vtx G Fin N WWalksN G Fin
34 25 33 pm2.61i Vtx G Fin N WWalksN G Fin