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 ∅ )