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	⊢ 1s = ( { 0s } |s ∅ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1s	⊢ 1s
1		c0s	⊢ 0s
2	1	csn	⊢ { 0s }
3		cscut	⊢ |s
4		c0	⊢ ∅
5	2 4 3	co	⊢ ( { 0s } |s ∅ )
6	0 5	wceq	⊢ 1s = ( { 0s } |s ∅ )