Theorem pfxnndmnd

Description: The value of a prefix operation for out-of-domain arguments. (This is due to our definition of function values for out-of-domain arguments, see ndmfv ). (Contributed by AV, 3-Dec-2022) (New usage is discouraged.)

	Ref	Expression
Assertion	pfxnndmnd	$$⊢\neg \left(S\in \mathrm{V}\wedge L\in {\mathbb{N}}_0\right)\to S\mathrm{prefix}L=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-pfx	$$⊢\mathrm{prefix}=\left(s\in \mathrm{V},l\in {\mathbb{N}}_0⟼s\mathrm{substr}⟨0,l⟩\right)$$
2	1	mpondm0	$$⊢\neg \left(S\in \mathrm{V}\wedge L\in {\mathbb{N}}_0\right)\to S\mathrm{prefix}L=\varnothing$$