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 Word V V W 0 lastS W

Proof

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