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 ‘ 𝑊 ) ∈ 𝑉 )