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	Could not format assertion : No typesetting found for |- 1s = ( { 0s } |s (/) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1s	Could not format 1s : No typesetting found for class 1s with typecode class
1		c0s	Could not format 0s : No typesetting found for class 0s with typecode class
2	1	csn	Could not format { 0s } : No typesetting found for class { 0s } with typecode class
3		cscut	$$class{|}_s$$
4		c0	$$class\varnothing$$
5	2 4 3	co	Could not format ( { 0s } |s (/) ) : No typesetting found for class ( { 0s } |s (/) ) with typecode class
6	0 5	wceq	Could not format 1s = ( { 0s } |s (/) ) : No typesetting found for wff 1s = ( { 0s } |s (/) ) with typecode wff