Definition df-0s

Description: Define surreal zero. This is the simplest cut of surreal number sets. Definition from Conway p. 17. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	df-0s	$$⊢0_s=\varnothing {|}_s\varnothing$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0s	$$class{0}_s$$
1		c0	$$class\varnothing$$
2		cscut	$$class{|}_s$$
3	1 1 2	co	$$class\left(\varnothing {|}_s\varnothing \right)$$
4	0 3	wceq	$$wff{0}_s=\varnothing {|}_s\varnothing$$