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 ) ∈ 𝑉 )