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 ⊢ W ∈ Word V ∧ 1 ≤ W → W ⁡ 0 ∈ V

Proof

Step Hyp Ref Expression
1 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
2 elnnnn0c ⊢ W ∈ ℕ ↔ W ∈ ℕ 0 ∧ 1 ≤ W
3 2 biimpri ⊢ W ∈ ℕ 0 ∧ 1 ≤ W → W ∈ ℕ
4 1 3 sylan ⊢ W ∈ Word V ∧ 1 ≤ W → W ∈ ℕ
5 lbfzo0 ⊢ 0 ∈ 0 ..^ W ↔ W ∈ ℕ
6 4 5 sylibr ⊢ W ∈ Word V ∧ 1 ≤ W → 0 ∈ 0 ..^ W
7 wrdsymbcl ⊢ W ∈ Word V ∧ 0 ∈ 0 ..^ W → W ⁡ 0 ∈ V
8 6 7 syldan ⊢ W ∈ Word V ∧ 1 ≤ W → W ⁡ 0 ∈ V