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	|- 0s = ( (/) |s (/) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0s	|- 0s
1		c0	|- (/)
2		cscut	|- |s
3	1 1 2	co	|- ( (/) |s (/) )
4	0 3	wceq	|- 0s = ( (/) |s (/) )