Metamath Proof Explorer


Definition df-1s

Description: Define surreal one. This is the simplest number greater than surreal zero. Definition from Conway p. 18. (Contributed by Scott Fenton, 7-Aug-2024)

Ref Expression
Assertion df-1s
|- 1s = ( { 0s } |s (/) )

Detailed syntax breakdown

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