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 𝐴 )