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