Definition df-2s

Description: Define surreal two. This is the simplest number greater than one. See 1p1e2s for its addition version. (Contributed by Scott Fenton, 27-May-2025)

	Ref	Expression
Assertion	df-2s	Could not format assertion : No typesetting found for |- 2s = ( { 1s } |s (/) ) with typecode |-

Detailed syntax breakdown

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