Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bday | Structured version Visualization version Unicode version |
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.) |
Ref | Expression |
---|---|
df-bday |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbday 31795 | . 2 | |
2 | vx | . . 3 | |
3 | csur 31793 | . . 3 | |
4 | 2 | cv 1482 | . . . 4 |
5 | 4 | cdm 5114 | . . 3 |
6 | 2, 3, 5 | cmpt 4729 | . 2 |
7 | 1, 6 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: bdayval 31801 bdayfo 31828 |
Copyright terms: Public domain | W3C validator |