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→NWWalksNG∈Fin

Proof

Step Hyp Ref Expression
1 wrdnfi ⊢Vtx⁡G∈Fin→w∈WordVtx⁡G|w=N+1∈Fin
2 simpr ⊢w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1→w=N+1
3 2 a1i ⊢w∈WordVtx⁡G→w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1→w=N+1
4 3 ss2rabi ⊢w∈WordVtx⁡G|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1⊆w∈WordVtx⁡G|w=N+1
5 4 a1i ⊢Vtx⁡G∈Fin→w∈WordVtx⁡G|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1⊆w∈WordVtx⁡G|w=N+1
6 1 5 ssfid ⊢Vtx⁡G∈Fin→w∈WordVtx⁡G|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1∈Fin
7 wwlksn ⊢N∈ℕ0→NWWalksNG=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→NWWalksNG=w|w∈WWalks⁡G∧w=N+1
10 3anan12 ⊢w≠∅∧w∈WordVtx⁡G∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G↔w∈WordVtx⁡G∧w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G
11 10 anbi1i ⊢w≠∅∧w∈WordVtx⁡G∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1↔w∈WordVtx⁡G∧w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1
12 anass ⊢w∈WordVtx⁡G∧w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1↔w∈WordVtx⁡G∧w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1
13 11 12 bitri ⊢w≠∅∧w∈WordVtx⁡G∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1↔w∈WordVtx⁡G∧w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1
14 13 abbii ⊢w|w≠∅∧w∈WordVtx⁡G∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1=w|w∈WordVtx⁡G∧w≠∅∧∀i∈0..^w−1w⁡iw⁡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∈WordVtx⁡G∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G
18 17 anbi1i ⊢w∈WWalks⁡G∧w=N+1↔w≠∅∧w∈WordVtx⁡G∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1
19 18 abbii ⊢w|w∈WWalks⁡G∧w=N+1=w|w≠∅∧w∈WordVtx⁡G∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1
20 df-rab ⊢w∈WordVtx⁡G|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1=w|w∈WordVtx⁡G∧w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1
21 14 19 20 3eqtr4i ⊢w|w∈WWalks⁡G∧w=N+1=w∈WordVtx⁡G|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1
22 9 21 eqtrdi ⊢N∈ℕ0→NWWalksNG=w∈WordVtx⁡G|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1
23 22 eleq1d ⊢N∈ℕ0→NWWalksNG∈Fin↔w∈WordVtx⁡G|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡G∧w=N+1∈Fin
24 6 23 imbitrrid ⊢N∈ℕ0→Vtx⁡G∈Fin→NWWalksNG∈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→NWWalksNG=∅
29 27 28 syl ⊢¬N∈ℕ0→NWWalksNG=∅
30 0fin ⊢∅∈Fin
31 29 30 eqeltrdi ⊢¬N∈ℕ0→NWWalksNG∈Fin
32 31 a1d ⊢¬N∈ℕ0→Vtx⁡G∈Fin→NWWalksNG∈Fin
33 24 32 pm2.61i ⊢Vtx⁡G∈Fin→NWWalksNG∈Fin