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∈WordV∧∅∉V∧W≠0→lastS⁡W≠∅

Proof

Step Hyp Ref Expression
1 lsw ⊢W∈WordV→lastS⁡W=W⁡W−1
2 1 3ad2ant1 ⊢W∈WordV∧∅∉V∧W≠0→lastS⁡W=W⁡W−1
3 wrdf ⊢W∈WordV→W:0..^W⟶V
4 lencl ⊢W∈WordV→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 ffvelcdmd ⊢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∈WordV→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 imbitrrdi ⊢W⁡W−1∈V→W⁡W−1=∅→¬∅∉V
25 24 necon2ad ⊢W⁡W−1∈V→∅∉V→W⁡W−1≠∅
26 18 25 syl6 ⊢W∈WordV→W≠0→∅∉V→W⁡W−1≠∅
27 26 com23 ⊢W∈WordV→∅∉V→W≠0→W⁡W−1≠∅
28 27 3imp ⊢W∈WordV∧∅∉V∧W≠0→W⁡W−1≠∅
29 2 28 eqnetrd ⊢W∈WordV∧∅∉V∧W≠0→lastS⁡W≠∅