pfx0

Description: A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020)

		Ref	Expression
	Assertion	pfx0	$⊢ \emptyset prefix L = \emptyset$

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨\emptyset, L⟩ \in (V \times ℕ_{0}) \leftrightarrow (\emptyset \in V \land L \in ℕ_{0})$
2		pfxval	$⊢ (\emptyset \in V \land L \in ℕ_{0}) \to \emptyset prefix L = \emptyset substr ⟨0, L⟩$
3		swrd0	$⊢ \emptyset substr ⟨0, L⟩ = \emptyset$
4	2 3	eqtrdi	$⊢ (\emptyset \in V \land L \in ℕ_{0}) \to \emptyset prefix L = \emptyset$
5	1 4	sylbi	$⊢ ⟨\emptyset, L⟩ \in (V \times ℕ_{0}) \to \emptyset prefix L = \emptyset$
6		df-pfx	$⊢ prefix = (s \in V, l \in ℕ_{0} ⟼ s substr ⟨0, l⟩)$
7		ovex	$⊢ s substr ⟨0, l⟩ \in V$
8	6 7	dmmpo	$⊢ dom prefix = V \times ℕ_{0}$
9	5 8	eleq2s	$⊢ ⟨\emptyset, L⟩ \in dom prefix \to \emptyset prefix L = \emptyset$
10		df-ov	$⊢ \emptyset prefix L = prefix (⟨\emptyset, L⟩)$
11		ndmfv	$⊢ \neg ⟨\emptyset, L⟩ \in dom prefix \to prefix (⟨\emptyset, L⟩) = \emptyset$
12	10 11	eqtrid	$⊢ \neg ⟨\emptyset, L⟩ \in dom prefix \to \emptyset prefix L = \emptyset$
13	9 12	pm2.61i	$⊢ \emptyset prefix L = \emptyset$

Metamath Proof Explorer