Metamath Proof Explorer

Theorem pfxcl

Description: Closure of the prefix extractor. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion pfxcl ⊢ S ∈ Word A → S prefix L ∈ Word A

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ S prefix L = ∅ → S prefix L ∈ Word A ↔ ∅ ∈ Word A
2 n0 ⊢ S prefix L ≠ ∅ ↔ ∃ x x ∈ S prefix L
3 df-pfx ⊢ prefix = s ∈ V , l ∈ ℕ 0 ⟼ s substr 0 l
4 3 elmpocl2 ⊢ x ∈ S prefix L → L ∈ ℕ 0
5 4 exlimiv ⊢ ∃ x x ∈ S prefix L → L ∈ ℕ 0
6 2 5 sylbi ⊢ S prefix L ≠ ∅ → L ∈ ℕ 0
7 pfxval ⊢ S ∈ Word A ∧ L ∈ ℕ 0 → S prefix L = S substr 0 L
8 swrdcl ⊢ S ∈ Word A → S substr 0 L ∈ Word A
9 8 adantr ⊢ S ∈ Word A ∧ L ∈ ℕ 0 → S substr 0 L ∈ Word A
10 7 9 eqeltrd ⊢ S ∈ Word A ∧ L ∈ ℕ 0 → S prefix L ∈ Word A
11 6 10 sylan2 ⊢ S ∈ Word A ∧ S prefix L ≠ ∅ → S prefix L ∈ Word A
12 wrd0 ⊢ ∅ ∈ Word A
13 12 a1i ⊢ S ∈ Word A → ∅ ∈ Word A
14 1 11 13 pm2.61ne ⊢ S ∈ Word A → S prefix L ∈ Word A