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

Detailed syntax breakdown

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