Metamath Proof Explorer

Theorem lswcl

Description: Closure of the last symbol: the last symbol of a not empty 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∈WordV∧W≠∅→lastS⁡W∈V

Proof

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