MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-2s Structured version   Visualization version   GIF version

Definition df-2s 28404
Description: Define surreal two. This is the simplest number greater than one. See 1p1e2s 28409 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
StepHypRef Expression
1 c2s 28403 . 2 class 2s
2 c1s 27877 . . . 4 class 1s
32csn 4648 . . 3 class { 1s }
4 c0 4347 . . 3 class
5 cscut 27836 . . 3 class |s
63, 4, 5co 7445 . 2 class ({ 1s } |s ∅)
71, 6wceq 1537 1 wff 2s = ({ 1s } |s ∅)
Colors of variables: wff setvar class
This definition is referenced by:  1p1e2s  28409
  Copyright terms: Public domain W3C validator