Metamath Proof Explorer

Theorem lswlgt0cl

Description: The last symbol of a nonempty word is an element of the alphabet for the word. (Contributed by Alexander van der Vekens, 1-Oct-2018) (Proof shortened by AV, 29-Apr-2020)

Ref Expression
Assertion lswlgt0cl ⊢ N ∈ ℕ ∧ W ∈ Word V ∧ W = N → lastS ⁡ W ∈ V

Proof

Step Hyp Ref Expression
1 simprl ⊢ N ∈ ℕ ∧ W ∈ Word V ∧ W = N → W ∈ Word V
2 eleq1 ⊢ N = W → N ∈ ℕ ↔ W ∈ ℕ
3 2 eqcoms ⊢ W = N → N ∈ ℕ ↔ W ∈ ℕ
4 3 adantl ⊢ W ∈ Word V ∧ W = N → N ∈ ℕ ↔ W ∈ ℕ
5 wrdfin ⊢ W ∈ Word V → W ∈ Fin
6 hashnncl ⊢ W ∈ Fin → W ∈ ℕ ↔ W ≠ ∅
7 5 6 syl ⊢ W ∈ Word V → W ∈ ℕ ↔ W ≠ ∅
8 7 biimpd ⊢ W ∈ Word V → W ∈ ℕ → W ≠ ∅
9 8 adantr ⊢ W ∈ Word V ∧ W = N → W ∈ ℕ → W ≠ ∅
10 4 9 sylbid ⊢ W ∈ Word V ∧ W = N → N ∈ ℕ → W ≠ ∅
11 10 impcom ⊢ N ∈ ℕ ∧ W ∈ Word V ∧ W = N → W ≠ ∅
12 lswcl ⊢ W ∈ Word V ∧ W ≠ ∅ → lastS ⁡ W ∈ V
13 1 11 12 syl2anc ⊢ N ∈ ℕ ∧ W ∈ Word V ∧ W = N → lastS ⁡ W ∈ V