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

Metamath Proof Explorer

Theorem fstwrdne0

Description: The first symbol of a nonempty word is an 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 ) ∈ 𝑉 )