Definition df-1s

Description: Define surreal one. This is the simplest number greater than surreal zero. Definition from Conway p. 18. (Contributed by Scott Fenton, 7-Aug-2024)

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

Detailed syntax breakdown

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