Theorem nulslts

Description: The empty set is less-than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Assertion	nulslts	$$⊢A\in 𝒫\mathrm{No}\to \varnothing {\ll }_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2	1	a1i	$$⊢A\in 𝒫\mathrm{No}\to \varnothing \in \mathrm{V}$$
3		elex	$$⊢A\in 𝒫\mathrm{No}\to A\in \mathrm{V}$$
4		0ss	$$⊢\varnothing \subseteq \mathrm{No}$$
5	4	a1i	$$⊢A\in 𝒫\mathrm{No}\to \varnothing \subseteq \mathrm{No}$$
6		elpwi	$$⊢A\in 𝒫\mathrm{No}\to A\subseteq \mathrm{No}$$
7		noel	$$⊢\neg x\in \varnothing$$
8	7	pm2.21i	$$⊢x\in \varnothing \to x{<}_{s}y$$
9	8	3ad2ant2	$$⊢\left(A\in 𝒫\mathrm{No}\wedge x\in \varnothing \wedge y\in A\right)\to x{<}_{s}y$$
10	2 3 5 6 9	sltsd	$$⊢A\in 𝒫\mathrm{No}\to \varnothing {\ll }_{s}A$$