Theorem lswlgt0cl

Description: The last symbol of a nonempty word is 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 e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( lastS ` W ) e. V )

Proof

Step	Hyp	Ref	Expression
1		simprl	|- ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> W e. Word V )
2		eleq1	|- ( N = ( # ` W ) -> ( N e. NN <-> ( # ` W ) e. NN ) )
3	2	eqcoms	|- ( ( # ` W ) = N -> ( N e. NN <-> ( # ` W ) e. NN ) )
4	3	adantl	|- ( ( W e. Word V /\ ( # ` W ) = N ) -> ( N e. NN <-> ( # ` W ) e. NN ) )
5		wrdfin	|- ( W e. Word V -> W e. Fin )
6		hashnncl	|- ( W e. Fin -> ( ( # ` W ) e. NN <-> W =/= (/) ) )
7	5 6	syl	|- ( W e. Word V -> ( ( # ` W ) e. NN <-> W =/= (/) ) )
8	7	biimpd	|- ( W e. Word V -> ( ( # ` W ) e. NN -> W =/= (/) ) )
9	8	adantr	|- ( ( W e. Word V /\ ( # ` W ) = N ) -> ( ( # ` W ) e. NN -> W =/= (/) ) )
10	4 9	sylbid	|- ( ( W e. Word V /\ ( # ` W ) = N ) -> ( N e. NN -> W =/= (/) ) )
11	10	impcom	|- ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> W =/= (/) )
12		lswcl	|- ( ( W e. Word V /\ W =/= (/) ) -> ( lastS ` W ) e. V )
13	1 11 12	syl2anc	|- ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( lastS ` W ) e. V )