Metamath Proof Explorer

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

Proof

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