Theorem pfx0

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

	Ref	Expression
Assertion	pfx0	$$⊢\varnothing \mathrm{prefix}L=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		opelxp	$$⊢⟨\varnothing ,L⟩\in \left(\mathrm{V}\times {\mathbb{N}}_0\right)\leftrightarrow \left(\varnothing \in \mathrm{V}\wedge L\in {\mathbb{N}}_0\right)$$
2		pfxval	$$⊢\left(\varnothing \in \mathrm{V}\wedge L\in {\mathbb{N}}_0\right)\to \varnothing \mathrm{prefix}L=\varnothing \mathrm{substr}⟨0,L⟩$$
3		swrd0	$$⊢\varnothing \mathrm{substr}⟨0,L⟩=\varnothing$$
4	2 3	eqtrdi	$$⊢\left(\varnothing \in \mathrm{V}\wedge L\in {\mathbb{N}}_0\right)\to \varnothing \mathrm{prefix}L=\varnothing$$
5	1 4	sylbi	$$⊢⟨\varnothing ,L⟩\in \left(\mathrm{V}\times {\mathbb{N}}_0\right)\to \varnothing \mathrm{prefix}L=\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	$$⊢⟨\varnothing ,L⟩\in \mathrm{dom}\mathrm{prefix}\to \varnothing \mathrm{prefix}L=\varnothing$$
10		df-ov	$$⊢\varnothing \mathrm{prefix}L=\mathrm{prefix}\left(⟨\varnothing ,L⟩\right)$$
11		ndmfv	$$⊢\neg ⟨\varnothing ,L⟩\in \mathrm{dom}\mathrm{prefix}\to \mathrm{prefix}\left(⟨\varnothing ,L⟩\right)=\varnothing$$
12	10 11	eqtrid	$$⊢\neg ⟨\varnothing ,L⟩\in \mathrm{dom}\mathrm{prefix}\to \varnothing \mathrm{prefix}L=\varnothing$$
13	9 12	pm2.61i	$$⊢\varnothing \mathrm{prefix}L=\varnothing$$