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