Metamath Proof Explorer

Theorem pfxn0

Description: A prefix consisting of at least one symbol is not empty. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 2-May-2020)

Ref Expression
Assertion pfxn0 ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → W prefix L ≠ ∅

Proof

Step Hyp Ref Expression
1 lbfzo0 ⊢ 0 ∈ 0 ..^ L ↔ L ∈ ℕ
2 ne0i ⊢ 0 ∈ 0 ..^ L → 0 ..^ L ≠ ∅
3 1 2 sylbir ⊢ L ∈ ℕ → 0 ..^ L ≠ ∅
4 3 3ad2ant2 ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → 0 ..^ L ≠ ∅
5 simp1 ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → W ∈ Word V
6 nnnn0 ⊢ L ∈ ℕ → L ∈ ℕ 0
7 6 3ad2ant2 ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → L ∈ ℕ 0
8 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
9 8 3ad2ant1 ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → W ∈ ℕ 0
10 simp3 ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → L ≤ W
11 elfz2nn0 ⊢ L ∈ 0 … W ↔ L ∈ ℕ 0 ∧ W ∈ ℕ 0 ∧ L ≤ W
12 7 9 10 11 syl3anbrc ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → L ∈ 0 … W
13 pfxf ⊢ W ∈ Word V ∧ L ∈ 0 … W → W prefix L : 0 ..^ L ⟶ V
14 5 12 13 syl2anc ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → W prefix L : 0 ..^ L ⟶ V
15 f0dom0 ⊢ W prefix L : 0 ..^ L ⟶ V → 0 ..^ L = ∅ ↔ W prefix L = ∅
16 15 bicomd ⊢ W prefix L : 0 ..^ L ⟶ V → W prefix L = ∅ ↔ 0 ..^ L = ∅
17 14 16 syl ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → W prefix L = ∅ ↔ 0 ..^ L = ∅
18 17 necon3bid ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → W prefix L ≠ ∅ ↔ 0 ..^ L ≠ ∅
19 4 18 mpbird ⊢ W ∈ Word V ∧ L ∈ ℕ ∧ L ≤ W → W prefix L ≠ ∅