pfxcl

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

		Ref	Expression
	Assertion	pfxcl	$⊢ S \in Word A \to S prefix L \in Word A$

Step	Hyp	Ref	Expression
1		eleq1	$⊢ S prefix L = \emptyset \to (S prefix L \in Word A \leftrightarrow \emptyset \in Word A)$
2		n0	$⊢ S prefix L \neq \emptyset \leftrightarrow \exists x x \in (S prefix L)$
3		df-pfx	$⊢ prefix = (s \in V, l \in ℕ_{0} ⟼ s substr ⟨0, l⟩)$
4	3	elmpocl2	$⊢ x \in (S prefix L) \to L \in ℕ_{0}$
5	4	exlimiv	$⊢ \exists x x \in (S prefix L) \to L \in ℕ_{0}$
6	2 5	sylbi	$⊢ S prefix L \neq \emptyset \to L \in ℕ_{0}$
7		pfxval	$⊢ (S \in Word A \land L \in ℕ_{0}) \to S prefix L = S substr ⟨0, L⟩$
8		swrdcl	$⊢ S \in Word A \to S substr ⟨0, L⟩ \in Word A$
9	8	adantr	$⊢ (S \in Word A \land L \in ℕ_{0}) \to S substr ⟨0, L⟩ \in Word A$
10	7 9	eqeltrd	$⊢ (S \in Word A \land L \in ℕ_{0}) \to S prefix L \in Word A$
11	6 10	sylan2	$⊢ (S \in Word A \land S prefix L \neq \emptyset) \to S prefix L \in Word A$
12		wrd0	$⊢ \emptyset \in Word A$
13	12	a1i	$⊢ S \in Word A \to \emptyset \in Word A$
14	1 11 13	pm2.61ne	$⊢ S \in Word A \to S prefix L \in Word A$

Metamath Proof Explorer