Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-no Unicode version

Definition df-no 24297
Description: Define the class of surreal numbers. The surreal numbers are a proper class of numbers developed by John H. Conway and introduced by Donald Knuth in 1975. They form a proper class into which all ordered fields can be embedded. The approach we take to defining them was first introduced by Hary Goshnor, and is based on the conception of a "sign expansion" of a surreal number. We define the surreals as ordinal-indexed sequences of 
1o and  2o, analagous to Goshnor's  (  -  ) and  (  +  ).

After introducing this definition, we will abstract away from it using axioms that Norman Alling developed in "Foundations of Analysis over Surreal Number Fields." This is done in a effort to be agnostic towards the exact implementation of surreals. (Contributed by Scott Fenton, 9-Jun-2011.)

Assertion
Ref Expression
df-no  |-  No  =  { f  |  E. a  e.  On  f : a --> { 1o ,  2o } }
Distinct variable group:    f, a

Detailed syntax breakdown of Definition df-no
StepHypRef Expression
1 csur 24294 . 2  class  No
2 va . . . . . 6  set  a
32cv 1622 . . . . 5  class  a
4 c1o 6472 . . . . . 6  class  1o
5 c2o 6473 . . . . . 6  class  2o
64, 5cpr 3641 . . . . 5  class  { 1o ,  2o }
7 vf . . . . . 6  set  f
87cv 1622 . . . . 5  class  f
93, 6, 8wf 5251 . . . 4  wff  f : a --> { 1o ,  2o }
10 con0 4392 . . . 4  class  On
119, 2, 10wrex 2544 . . 3  wff  E. a  e.  On  f : a --> { 1o ,  2o }
1211, 7cab 2269 . 2  class  { f  |  E. a  e.  On  f : a --> { 1o ,  2o } }
131, 12wceq 1623 1  wff  No  =  { f  |  E. a  e.  On  f : a --> { 1o ,  2o } }
Colors of variables: wff set class
This definition is referenced by:  elno  24300  sltso  24323
  Copyright terms: Public domain W3C validator