This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( lastS ‘ 𝑊 ) = ∅ )

Proof

Step Hyp Ref Expression
1 lsw ⊢ ( 𝑊 ∈ Word 𝑉 → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
2 1 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
3 fvoveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( 0 − 1 ) ) )
4 wrddm ⊢ ( 𝑊 ∈ Word 𝑉 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
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 ..^ ( ♯ ‘ 𝑊 ) ) → 0 ≤ ( 0 − 1 ) )
13 11 12 mto ⊢ ¬ ( 0 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) )
14 eleq2 ⊢ ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 0 − 1 ) ∈ dom 𝑊 ↔ ( 0 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
15 13 14 mtbiri ⊢ ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ¬ ( 0 − 1 ) ∈ dom 𝑊 )
16 ndmfv ⊢ ( ¬ ( 0 − 1 ) ∈ dom 𝑊 → ( 𝑊 ‘ ( 0 − 1 ) ) = ∅ )
17 4 15 16 3syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ‘ ( 0 − 1 ) ) = ∅ )
18 3 17 sylan9eqr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ∅ )
19 2 18 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( lastS ‘ 𝑊 ) = ∅ )