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 ( ( 𝑊 ∈ 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 ffvelrnd ( ( ( 𝑊 : ( 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 syl6ibr ( ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 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 ‘ 𝑊 ) ≠ ∅ )