Definition df-2s 28350

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

Assertion

Ref	Expression
df-2s	⊢ 2s = ({ 1s } |s ∅)

Detailed syntax breakdown of Definition df-2s

Step	Hyp	Ref	Expression
1		c2s 28349	. 2 class 2s
2		c1s 27823	. . . 4 class 1s
3	2	csn 4608	. . 3 class { 1s }
4		c0 4315	. . 3 class ∅
5		cscut 27782	. . 3 class |s
6	3, 4, 5	co 7414	. 2 class ({ 1s } |s ∅)
7	1, 6	wceq 1539	1 wff 2s = ({ 1s } |s ∅)

This definition is referenced by:  1p1e2s  28355