Definition df-0s 27805

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

Assertion

Ref	Expression
df-0s	⊢ 0s = (∅ |s ∅)

Detailed syntax breakdown of Definition df-0s

Step	Hyp	Ref	Expression
1		c0s 27803	. 2 class 0s
2		c0 4286	. . 3 class ∅
3		cscut 27759	. . 3 class |s
4	2, 2, 3	co 7360	. 2 class (∅ |s ∅)
5	1, 4	wceq 1542	1 wff 0s = (∅ |s ∅)

This definition is referenced by:  0sno  27807  bday0s  27809  0slt1s  27810  bday0b  27811  rightpos  27819  made0  27855  negs0s  28008  muls01  28094  n0sfincut  28335