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 ⊢ N ∈ ℕ ∧ W ∈ Word V ∧ W = N → W ⁡ 0 ∈ V

Proof

Step Hyp Ref Expression
1 simprl ⊢ N ∈ ℕ ∧ W ∈ Word V ∧ W = N → W ∈ Word V
2 nnge1 ⊢ N ∈ ℕ → 1 ≤ N
3 2 adantr ⊢ N ∈ ℕ ∧ W ∈ Word V ∧ W = N → 1 ≤ N
4 breq2 ⊢ W = N → 1 ≤ W ↔ 1 ≤ N
5 4 ad2antll ⊢ N ∈ ℕ ∧ W ∈ Word V ∧ W = N → 1 ≤ W ↔ 1 ≤ N
6 3 5 mpbird ⊢ N ∈ ℕ ∧ W ∈ Word V ∧ W = N → 1 ≤ W
7 wrdsymb1 ⊢ W ∈ Word V ∧ 1 ≤ W → W ⁡ 0 ∈ V
8 1 6 7 syl2anc ⊢ N ∈ ℕ ∧ W ∈ Word V ∧ W = N → W ⁡ 0 ∈ V