Theorem nulssgt

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

	Ref	Expression
Assertion	nulssgt	$$⊢A\in 𝒫\mathrm{No}\to A{\ll }_s\varnothing$$

Proof

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