Metamath Proof Explorer

Theorem lswn0

Description: The last symbol of a nonempty 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 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 ∈ 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 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 ∈ 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 ≠ ∅