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

Definition df-bday 32125
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 = (𝑥 No ↦ dom 𝑥)

Detailed syntax breakdown of Definition df-bday
StepHypRef Expression
1 cbday 32122 . 2 class bday
2 vx . . 3 setvar 𝑥
3 csur 32120 . . 3 class No
42cv 1631 . . . 4 class 𝑥
54cdm 5266 . . 3 class dom 𝑥
62, 3, 5cmpt 4881 . 2 class (𝑥 No ↦ dom 𝑥)
71, 6wceq 1632 1 wff bday = (𝑥 No ↦ dom 𝑥)
Colors of variables: wff setvar class
This definition is referenced by:  bdayval  32128  bdayfo  32155
  Copyright terms: Public domain W3C validator