Metamath Proof Explorer

Theorem lsw0

Description: The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 19-Mar-2018) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion lsw0 ⊢ W ∈ Word V ∧ W = 0 → lastS ⁡ W = ∅

Proof

Step Hyp Ref Expression
1 lsw ⊢ W ∈ Word V → lastS ⁡ W = W ⁡ W − 1
2 1 adantr ⊢ W ∈ Word V ∧ W = 0 → lastS ⁡ W = W ⁡ W − 1
3 fvoveq1 ⊢ W = 0 → W ⁡ W − 1 = W ⁡ 0 − 1
4 wrddm ⊢ W ∈ Word V → dom ⁡ W = 0 ..^ W
5 1nn ⊢ 1 ∈ ℕ
6 nnnle0 ⊢ 1 ∈ ℕ → ¬ 1 ≤ 0
7 5 6 ax-mp ⊢ ¬ 1 ≤ 0
8 0re ⊢ 0 ∈ ℝ
9 1re ⊢ 1 ∈ ℝ
10 8 9 subge0i ⊢ 0 ≤ 0 − 1 ↔ 1 ≤ 0
11 7 10 mtbir ⊢ ¬ 0 ≤ 0 − 1
12 elfzole1 ⊢ 0 − 1 ∈ 0 ..^ W → 0 ≤ 0 − 1
13 11 12 mto ⊢ ¬ 0 − 1 ∈ 0 ..^ W
14 eleq2 ⊢ dom ⁡ W = 0 ..^ W → 0 − 1 ∈ dom ⁡ W ↔ 0 − 1 ∈ 0 ..^ W
15 13 14 mtbiri ⊢ dom ⁡ W = 0 ..^ W → ¬ 0 − 1 ∈ dom ⁡ W
16 ndmfv ⊢ ¬ 0 − 1 ∈ dom ⁡ W → W ⁡ 0 − 1 = ∅
17 4 15 16 3syl ⊢ W ∈ Word V → W ⁡ 0 − 1 = ∅
18 3 17 sylan9eqr ⊢ W ∈ Word V ∧ W = 0 → W ⁡ W − 1 = ∅
19 2 18 eqtrd ⊢ W ∈ Word V ∧ W = 0 → lastS ⁡ W = ∅