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	|- 2s = ( { 1s } |s (/) )

Detailed syntax breakdown

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