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 ffvelcdmd 
 |-  ( ( ( 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 imbitrrdi 
 |-  ( ( 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 ) =/= (/) )