This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑊 ‘ 𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 wwlknbp1 ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
2 simp2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
3 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
4 fzval3 ⊢ ( 𝑁 ∈ ℤ → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
5 3 4 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
6 5 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
7 6 eleq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ... 𝑁 ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
8 7 biimpa ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
9 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
10 9 eleq2d ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
11 10 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
12 11 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
13 8 12 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
14 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )
15 2 13 14 syl2an2r ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 ‘ 𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )
16 15 ralrimiva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑊 ‘ 𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )
17 1 16 syl ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑊 ‘ 𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )