Theorem nulsgtsd

Description: The empty set is greater 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	nulsgtsd	$$⊢\phi \to A{\ll }_s\varnothing$$

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		nulsgts	$$⊢A\in 𝒫\mathrm{No}\to A{\ll }_s\varnothing$$
5	3 4	syl	$$⊢\phi \to A{\ll }_s\varnothing$$