pfx00

Description: The zero length prefix is the empty set. (Contributed by AV, 2-May-2020)

		Ref	Expression
	Assertion	pfx00	$⊢ S prefix 0 = \emptyset$

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨S, 0⟩ \in (V \times ℕ_{0}) \leftrightarrow (S \in V \land 0 \in ℕ_{0})$
2		pfxval	$⊢ (S \in V \land 0 \in ℕ_{0}) \to S prefix 0 = S substr ⟨0, 0⟩$
3		swrd00	$⊢ S substr ⟨0, 0⟩ = \emptyset$
4	2 3	eqtrdi	$⊢ (S \in V \land 0 \in ℕ_{0}) \to S prefix 0 = \emptyset$
5	1 4	sylbi	$⊢ ⟨S, 0⟩ \in (V \times ℕ_{0}) \to S prefix 0 = \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	$⊢ ⟨S, 0⟩ \in dom prefix \to S prefix 0 = \emptyset$
10		df-ov	$⊢ S prefix 0 = prefix (⟨S, 0⟩)$
11		ndmfv	$⊢ \neg ⟨S, 0⟩ \in dom prefix \to prefix (⟨S, 0⟩) = \emptyset$
12	10 11	eqtrid	$⊢ \neg ⟨S, 0⟩ \in dom prefix \to S prefix 0 = \emptyset$
13	9 12	pm2.61i	$⊢ S prefix 0 = \emptyset$

Metamath Proof Explorer