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

Proof

Step Hyp Ref Expression
1 lsw ⊢ ( 𝑊 ∈ Word 𝑉 → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
2 1 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ∉ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
3 wrdf ⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 )
4 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
5 simpll ⊢ ( ( ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 )
6 elnnne0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) )
7 6 biimpri ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
8 nnm1nn0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 )
9 7 8 syl ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 )
10 nn0re ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
11 10 ltm1d ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) − 1 ) < ( ♯ ‘ 𝑊 ) )
12 11 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) < ( ♯ ‘ 𝑊 ) )
13 elfzo0 ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) < ( ♯ ‘ 𝑊 ) ) )
14 9 7 12 13 syl3anbrc ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
15 14 adantll ⊢ ( ( ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
16 5 15 ffvelcdmd ⊢ ( ( ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ 𝑉 )
17 16 ex ⊢ ( ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ 𝑉 ) )
18 3 4 17 syl2anc ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ 𝑉 ) )
19 eleq1a ⊢ ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ 𝑉 → ( ∅ = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ∅ ∈ 𝑉 ) )
20 19 com12 ⊢ ( ∅ = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ 𝑉 → ∅ ∈ 𝑉 ) )
21 20 eqcoms ⊢ ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ∅ → ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ 𝑉 → ∅ ∈ 𝑉 ) )
22 21 com12 ⊢ ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ 𝑉 → ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ∅ → ∅ ∈ 𝑉 ) )
23 nnel ⊢ ( ¬ ∅ ∉ 𝑉 ↔ ∅ ∈ 𝑉 )
24 22 23 imbitrrdi ⊢ ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ 𝑉 → ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ∅ → ¬ ∅ ∉ 𝑉 ) )
25 24 necon2ad ⊢ ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ 𝑉 → ( ∅ ∉ 𝑉 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ ) )
26 18 25 syl6 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ∅ ∉ 𝑉 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ ) ) )
27 26 com23 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ∅ ∉ 𝑉 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ ) ) )
28 27 3imp ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ∉ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ )
29 2 28 eqnetrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ∉ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( lastS ‘ 𝑊 ) ≠ ∅ )