Theorem pfx00

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

	Ref	Expression
Assertion	pfx00	$$⊢S\mathrm{prefix}0=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		opelxp	$$⊢⟨S,0⟩\in \left(\mathrm{V}\times {\mathbb{N}}_0\right)\leftrightarrow \left(S\in \mathrm{V}\wedge 0\in {\mathbb{N}}_0\right)$$
2		pfxval	$$⊢\left(S\in \mathrm{V}\wedge 0\in {\mathbb{N}}_0\right)\to S\mathrm{prefix}0=S\mathrm{substr}⟨0,0⟩$$
3		swrd00	$$⊢S\mathrm{substr}⟨0,0⟩=\varnothing$$
4	2 3	eqtrdi	$$⊢\left(S\in \mathrm{V}\wedge 0\in {\mathbb{N}}_0\right)\to S\mathrm{prefix}0=\varnothing$$
5	1 4	sylbi	$$⊢⟨S,0⟩\in \left(\mathrm{V}\times {\mathbb{N}}_0\right)\to S\mathrm{prefix}0=\varnothing$$
6		df-pfx	$$⊢\mathrm{prefix}=\left(s\in \mathrm{V},l\in {\mathbb{N}}_0⟼s\mathrm{substr}⟨0,l⟩\right)$$
7		ovex	$$⊢s\mathrm{substr}⟨0,l⟩\in \mathrm{V}$$
8	6 7	dmmpo	$$⊢\mathrm{dom}\mathrm{prefix}=\mathrm{V}\times {\mathbb{N}}_0$$
9	5 8	eleq2s	$$⊢⟨S,0⟩\in \mathrm{dom}\mathrm{prefix}\to S\mathrm{prefix}0=\varnothing$$
10		df-ov	$$⊢S\mathrm{prefix}0=\mathrm{prefix}\left(⟨S,0⟩\right)$$
11		ndmfv	$$⊢\neg ⟨S,0⟩\in \mathrm{dom}\mathrm{prefix}\to \mathrm{prefix}\left(⟨S,0⟩\right)=\varnothing$$
12	10 11	syl5eq	$$⊢\neg ⟨S,0⟩\in \mathrm{dom}\mathrm{prefix}\to S\mathrm{prefix}0=\varnothing$$
13	9 12	pm2.61i	$$⊢S\mathrm{prefix}0=\varnothing$$