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 ‘ 𝐺 ) )