Metamath Proof Explorer

Theorem wwlknvtx

Description: The symbols of a word W representing a walk of a fixed length N are vertices. (Contributed by AV, 16-Mar-2022)

Ref Expression
Assertion wwlknvtx ⊢ W ∈ N WWalksN G → ∀ i ∈ 0 … N W ⁡ i ∈ Vtx ⁡ G

Proof

Step Hyp Ref Expression
1 wwlknbp1 ⊢ W ∈ N WWalksN G → N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1
2 simp2 ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → W ∈ Word Vtx ⁡ G
3 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
4 fzval3 ⊢ N ∈ ℤ → 0 … N = 0 ..^ N + 1
5 3 4 syl ⊢ N ∈ ℕ 0 → 0 … N = 0 ..^ N + 1
6 5 3ad2ant1 ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → 0 … N = 0 ..^ N + 1
7 6 eleq2d ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → i ∈ 0 … N ↔ i ∈ 0 ..^ N + 1
8 7 biimpa ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ i ∈ 0 … N → i ∈ 0 ..^ N + 1
9 oveq2 ⊢ W = N + 1 → 0 ..^ W = 0 ..^ N + 1
10 9 eleq2d ⊢ W = N + 1 → i ∈ 0 ..^ W ↔ i ∈ 0 ..^ N + 1
11 10 3ad2ant3 ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → i ∈ 0 ..^ W ↔ i ∈ 0 ..^ N + 1
12 11 adantr ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ i ∈ 0 … N → i ∈ 0 ..^ W ↔ i ∈ 0 ..^ N + 1
13 8 12 mpbird ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ i ∈ 0 … N → i ∈ 0 ..^ W
14 wrdsymbcl ⊢ W ∈ Word Vtx ⁡ G ∧ i ∈ 0 ..^ W → W ⁡ i ∈ Vtx ⁡ G
15 2 13 14 syl2an2r ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 ∧ i ∈ 0 … N → W ⁡ i ∈ Vtx ⁡ G
16 15 ralrimiva ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → ∀ i ∈ 0 … N W ⁡ i ∈ Vtx ⁡ G
17 1 16 syl ⊢ W ∈ N WWalksN G → ∀ i ∈ 0 … N W ⁡ i ∈ Vtx ⁡ G