Definition df-1s 27885

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

Assertion

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

Detailed syntax breakdown of Definition df-1s

Step	Hyp	Ref	Expression
1		c1s 27883	. 2 class 1s
2		c0s 27882	. . . 4 class 0s
3	2	csn 4631	. . 3 class { 0s }
4		c0 4339	. . 3 class ∅
5		cscut 27842	. . 3 class |s
6	3, 4, 5	co 7431	. 2 class ({ 0s } |s ∅)
7	1, 6	wceq 1537	1 wff 1s = ({ 0s } |s ∅)

This definition is referenced by:  1sno  27887  0slt1s  27889  bday1s  27891  n0scut  28353  1p1e2s  28415  nohalf  28422