Theorem 0no

Description: Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	0no	$$⊢0_s\in \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		df-0s	$$⊢0_s=\varnothing {|}_s\varnothing$$
2		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
3		nulsgts	$$⊢\varnothing \in 𝒫\mathrm{No}\to \varnothing {\ll }_s\varnothing$$
4	2 3	ax-mp	$$⊢\varnothing {\ll }_s\varnothing$$
5		cutscl	$$⊢\varnothing {\ll }_s\varnothing \to \varnothing {|}_s\varnothing \in \mathrm{No}$$
6	4 5	ax-mp	$$⊢\varnothing {|}_s\varnothing \in \mathrm{No}$$
7	1 6	eqeltri	$$⊢0_s\in \mathrm{No}$$