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 
|- ( ( 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 )