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 a1i ⊢ w ∈ Word Vtx ⁡ G → w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 → w = N + 1
4 3 ss2rabi ⊢ 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
5 4 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
6 1 5 ssfid ⊢ Vtx ⁡ G ∈ Fin → w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 ∈ Fin
7 wwlksn ⊢ N ∈ ℕ 0 → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1
8 df-rab ⊢ w ∈ WWalks ⁡ G | w = N + 1 = w | w ∈ WWalks ⁡ G ∧ w = N + 1
9 7 8 eqtrdi ⊢ N ∈ ℕ 0 → N WWalksN G = w | w ∈ WWalks ⁡ G ∧ w = N + 1
10 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
11 10 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
12 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
13 11 12 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
14 13 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
15 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
16 eqid ⊢ Edg ⁡ G = Edg ⁡ G
17 15 16 iswwlks ⊢ w ∈ WWalks ⁡ G ↔ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
18 17 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
19 18 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
20 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
21 14 19 20 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
22 9 21 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
23 22 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
24 6 23 imbitrrid ⊢ N ∈ ℕ 0 → Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin
25 df-nel ⊢ N ∉ ℕ 0 ↔ ¬ N ∈ ℕ 0
26 25 biimpri ⊢ ¬ N ∈ ℕ 0 → N ∉ ℕ 0
27 26 olcd ⊢ ¬ N ∈ ℕ 0 → G ∉ V ∨ N ∉ ℕ 0
28 wwlksnndef ⊢ G ∉ V ∨ N ∉ ℕ 0 → N WWalksN G = ∅
29 27 28 syl ⊢ ¬ N ∈ ℕ 0 → N WWalksN G = ∅
30 0fin ⊢ ∅ ∈ Fin
31 29 30 eqeltrdi ⊢ ¬ N ∈ ℕ 0 → N WWalksN G ∈ Fin
32 31 a1d ⊢ ¬ N ∈ ℕ 0 → Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin
33 24 32 pm2.61i ⊢ Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin