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 ∅ )