Theorem fstwrdne0

Description: The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 29-Sep-2018) (Proof shortened by AV, 14-Oct-2018)

	Ref	Expression
Assertion	fstwrdne0	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		simprl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → 𝑊 ∈ Word 𝑉 )
2		nnge1	⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
3	2	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → 1 ≤ 𝑁 )
4		breq2	⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 1 ≤ ( ♯ ‘ 𝑊 ) ↔ 1 ≤ 𝑁 ) )
5	4	ad2antll	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → ( 1 ≤ ( ♯ ‘ 𝑊 ) ↔ 1 ≤ 𝑁 ) )
6	3 5	mpbird	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → 1 ≤ ( ♯ ‘ 𝑊 ) )
7		wrdsymb1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
8	1 6 7	syl2anc	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )