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

Metamath Proof Explorer

Theorem wrdsymb1

Description: The first symbol of a nonempty word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018)

Ref Expression
Assertion wrdsymb1 ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
2 elnnnn0c ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) )
3 2 biimpri ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
4 1 3 sylan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
5 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ )
6 4 5 sylibr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
8 6 7 syldan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )