Metamath Proof Explorer

Theorem lswcl

Description: Closure of the last symbol: the last symbol of a nonempty word belongs to the alphabet for the word. (Contributed by AV, 2-Aug-2018) (Proof shortened by AV, 29-Apr-2020)

Ref Expression
Assertion lswcl ⊢ W ∈ Word V ∧ W ≠ ∅ → lastS ⁡ W ∈ V

Proof

Step Hyp Ref Expression
1 lsw ⊢ W ∈ Word V → lastS ⁡ W = W ⁡ W − 1
2 1 adantr ⊢ W ∈ Word V ∧ W ≠ ∅ → lastS ⁡ W = W ⁡ W − 1
3 lennncl ⊢ W ∈ Word V ∧ W ≠ ∅ → W ∈ ℕ
4 fzo0end ⊢ W ∈ ℕ → W − 1 ∈ 0 ..^ W
5 3 4 syl ⊢ W ∈ Word V ∧ W ≠ ∅ → W − 1 ∈ 0 ..^ W
6 wrdsymbcl ⊢ W ∈ Word V ∧ W − 1 ∈ 0 ..^ W → W ⁡ W − 1 ∈ V
7 5 6 syldan ⊢ W ∈ Word V ∧ W ≠ ∅ → W ⁡ W − 1 ∈ V
8 2 7 eqeltrd ⊢ W ∈ Word V ∧ W ≠ ∅ → lastS ⁡ W ∈ V