This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → ( lastS ‘ 𝑊 ) ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → 𝑊 ∈ Word 𝑉 )
2 eleq1 ⊢ ( 𝑁 = ( ♯ ‘ 𝑊 ) → ( 𝑁 ∈ ℕ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
3 2 eqcoms ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ∈ ℕ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
4 3 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑁 ∈ ℕ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
5 wrdfin ⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 ∈ Fin )
6 hashnncl ⊢ ( 𝑊 ∈ Fin → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ 𝑊 ≠ ∅ ) )
7 5 6 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ 𝑊 ≠ ∅ ) )
8 7 biimpd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → 𝑊 ≠ ∅ ) )
9 8 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → 𝑊 ≠ ∅ ) )
10 4 9 sylbid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑁 ∈ ℕ → 𝑊 ≠ ∅ ) )
11 10 impcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → 𝑊 ≠ ∅ )
12 lswcl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( lastS ‘ 𝑊 ) ∈ 𝑉 )
13 1 11 12 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → ( lastS ‘ 𝑊 ) ∈ 𝑉 )