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

Definition df-bday 28979
Description: Finally, we introduce the birthday function. This function maps each surreal to an ordinal. In our implementation, this is the domain of the sign function. The important properties of this function are established later. (Contributed by Scott Fenton, 11-Jun-2011.)
Assertion
Ref Expression
df-bday  |-  bday  =  ( x  e.  No  |->  dom  x )

Detailed syntax breakdown of Definition df-bday
StepHypRef Expression
1 cbday 28976 . 2  class  bday
2 vx . . 3  setvar  x
3 csur 28974 . . 3  class  No
42cv 1378 . . . 4  class  x
54cdm 4999 . . 3  class  dom  x
62, 3, 5cmpt 4505 . 2  class  ( x  e.  No  |->  dom  x
)
71, 6wceq 1379 1  wff  bday  =  ( x  e.  No  |->  dom  x )
Colors of variables: wff setvar class
This definition is referenced by:  bdayval  28982  bdayfo  29009
  Copyright terms: Public domain W3C validator