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

Metamath Proof Explorer

Theorem pfxcl

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

Ref Expression
Assertion pfxcl ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐿 ) ∈ Word 𝐴 )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( ( 𝑆 prefix 𝐿 ) = ∅ → ( ( 𝑆 prefix 𝐿 ) ∈ Word 𝐴 ↔ ∅ ∈ Word 𝐴 ) )
2 n0 ⊢ ( ( 𝑆 prefix 𝐿 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑆 prefix 𝐿 ) )
3 df-pfx ⊢ prefix = ( 𝑠 ∈ V , 𝑙 ∈ ℕ0 ↦ ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ ) )
4 3 elmpocl2 ⊢ ( 𝑥 ∈ ( 𝑆 prefix 𝐿 ) → 𝐿 ∈ ℕ0 )
5 4 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝑆 prefix 𝐿 ) → 𝐿 ∈ ℕ0 )
6 2 5 sylbi ⊢ ( ( 𝑆 prefix 𝐿 ) ≠ ∅ → 𝐿 ∈ ℕ0 )
7 pfxval ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 prefix 𝐿 ) = ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) )
8 swrdcl ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) ∈ Word 𝐴 )
9 8 adantr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) ∈ Word 𝐴 )
10 7 9 eqeltrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 prefix 𝐿 ) ∈ Word 𝐴 )
11 6 10 sylan2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝑆 prefix 𝐿 ) ≠ ∅ ) → ( 𝑆 prefix 𝐿 ) ∈ Word 𝐴 )
12 wrd0 ⊢ ∅ ∈ Word 𝐴
13 12 a1i ⊢ ( 𝑆 ∈ Word 𝐴 → ∅ ∈ Word 𝐴 )
14 1 11 13 pm2.61ne ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐿 ) ∈ Word 𝐴 )