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

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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix 𝐿 ) ≠ ∅ )

Proof

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