Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bday | Structured version Visualization version GIF 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 | ⊢ bday = (𝑥 ∈ No ↦ dom 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbday 33531 | . 2 class bday | |
2 | vx | . . 3 setvar 𝑥 | |
3 | csur 33529 | . . 3 class No | |
4 | 2 | cv 1542 | . . . 4 class 𝑥 |
5 | 4 | cdm 5536 | . . 3 class dom 𝑥 |
6 | 2, 3, 5 | cmpt 5120 | . 2 class (𝑥 ∈ No ↦ dom 𝑥) |
7 | 1, 6 | wceq 1543 | 1 wff bday = (𝑥 ∈ No ↦ dom 𝑥) |
Colors of variables: wff setvar class |
This definition is referenced by: bdayval 33537 bdayfo 33566 |
Copyright terms: Public domain | W3C validator |