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 Could not format assertion : No typesetting found for |- 1s = ( { 0s } |s (/) ) with typecode |-

Detailed syntax breakdown

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