Metamath Proof Explorer


Theorem lswn0

Description: The last symbol of a not empty word exists. The empty set must be excluded as symbol, because otherwise, it cannot be distinguished between valid cases ( (/) is the last symbol) and invalid cases ( (/) means that no last symbol exists. This is because of the special definition of a function in set.mm. (Contributed by Alexander van der Vekens, 18-Mar-2018)

Ref Expression
Assertion lswn0
|- ( ( W e. Word V /\ (/) e/ V /\ ( # ` W ) =/= 0 ) -> ( lastS ` W ) =/= (/) )

Proof

Step Hyp Ref Expression
1 lsw
 |-  ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
2 1 3ad2ant1
 |-  ( ( W e. Word V /\ (/) e/ V /\ ( # ` W ) =/= 0 ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
3 wrdf
 |-  ( W e. Word V -> W : ( 0 ..^ ( # ` W ) ) --> V )
4 lencl
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
5 simpll
 |-  ( ( ( W : ( 0 ..^ ( # ` W ) ) --> V /\ ( # ` W ) e. NN0 ) /\ ( # ` W ) =/= 0 ) -> W : ( 0 ..^ ( # ` W ) ) --> V )
6 elnnne0
 |-  ( ( # ` W ) e. NN <-> ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) )
7 6 biimpri
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) -> ( # ` W ) e. NN )
8 nnm1nn0
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. NN0 )
9 7 8 syl
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) -> ( ( # ` W ) - 1 ) e. NN0 )
10 nn0re
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. RR )
11 10 ltm1d
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - 1 ) < ( # ` W ) )
12 11 adantr
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) -> ( ( # ` W ) - 1 ) < ( # ` W ) )
13 elfzo0
 |-  ( ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) <-> ( ( ( # ` W ) - 1 ) e. NN0 /\ ( # ` W ) e. NN /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) )
14 9 7 12 13 syl3anbrc
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
15 14 adantll
 |-  ( ( ( W : ( 0 ..^ ( # ` W ) ) --> V /\ ( # ` W ) e. NN0 ) /\ ( # ` W ) =/= 0 ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
16 5 15 ffvelrnd
 |-  ( ( ( W : ( 0 ..^ ( # ` W ) ) --> V /\ ( # ` W ) e. NN0 ) /\ ( # ` W ) =/= 0 ) -> ( W ` ( ( # ` W ) - 1 ) ) e. V )
17 16 ex
 |-  ( ( W : ( 0 ..^ ( # ` W ) ) --> V /\ ( # ` W ) e. NN0 ) -> ( ( # ` W ) =/= 0 -> ( W ` ( ( # ` W ) - 1 ) ) e. V ) )
18 3 4 17 syl2anc
 |-  ( W e. Word V -> ( ( # ` W ) =/= 0 -> ( W ` ( ( # ` W ) - 1 ) ) e. V ) )
19 eleq1a
 |-  ( ( W ` ( ( # ` W ) - 1 ) ) e. V -> ( (/) = ( W ` ( ( # ` W ) - 1 ) ) -> (/) e. V ) )
20 19 com12
 |-  ( (/) = ( W ` ( ( # ` W ) - 1 ) ) -> ( ( W ` ( ( # ` W ) - 1 ) ) e. V -> (/) e. V ) )
21 20 eqcoms
 |-  ( ( W ` ( ( # ` W ) - 1 ) ) = (/) -> ( ( W ` ( ( # ` W ) - 1 ) ) e. V -> (/) e. V ) )
22 21 com12
 |-  ( ( W ` ( ( # ` W ) - 1 ) ) e. V -> ( ( W ` ( ( # ` W ) - 1 ) ) = (/) -> (/) e. V ) )
23 nnel
 |-  ( -. (/) e/ V <-> (/) e. V )
24 22 23 syl6ibr
 |-  ( ( W ` ( ( # ` W ) - 1 ) ) e. V -> ( ( W ` ( ( # ` W ) - 1 ) ) = (/) -> -. (/) e/ V ) )
25 24 necon2ad
 |-  ( ( W ` ( ( # ` W ) - 1 ) ) e. V -> ( (/) e/ V -> ( W ` ( ( # ` W ) - 1 ) ) =/= (/) ) )
26 18 25 syl6
 |-  ( W e. Word V -> ( ( # ` W ) =/= 0 -> ( (/) e/ V -> ( W ` ( ( # ` W ) - 1 ) ) =/= (/) ) ) )
27 26 com23
 |-  ( W e. Word V -> ( (/) e/ V -> ( ( # ` W ) =/= 0 -> ( W ` ( ( # ` W ) - 1 ) ) =/= (/) ) ) )
28 27 3imp
 |-  ( ( W e. Word V /\ (/) e/ V /\ ( # ` W ) =/= 0 ) -> ( W ` ( ( # ` W ) - 1 ) ) =/= (/) )
29 2 28 eqnetrd
 |-  ( ( W e. Word V /\ (/) e/ V /\ ( # ` W ) =/= 0 ) -> ( lastS ` W ) =/= (/) )