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 𝐿 ) ≠ ∅ )