Theorem nulsltsd

Description: The empty set is less-than any set of surreals. Deduction version. (Contributed by Scott Fenton, 27-Feb-2026)

	Ref	Expression
Hypotheses	nulsltsd.1	$$⊢\phi \to A\in V$$
	nulsltsd.2	$$⊢\phi \to A\subseteq \mathrm{No}$$
Assertion	nulsltsd	$$⊢\phi \to \varnothing {\ll }_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		nulsltsd.1	$$⊢\phi \to A\in V$$
2		nulsltsd.2	$$⊢\phi \to A\subseteq \mathrm{No}$$
3	1 2	elpwd	$$⊢\phi \to A\in 𝒫\mathrm{No}$$
4		nulslts	$$⊢A\in 𝒫\mathrm{No}\to \varnothing {\ll }_{s}A$$
5	3 4	syl	$$⊢\phi \to \varnothing {\ll }_{s}A$$