Definition df-bday 31042

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

Step	Hyp	Ref	Expression
1		cbday 31039	. 2 class bday
2		vx	. . 3 setvar 𝑥
3		csur 31037	. . 3 class No
4	2	cv 1474	. . . 4 class 𝑥
5	4	cdm 5038	. . 3 class dom 𝑥
6	2, 3, 5	cmpt 4643	. 2 class (𝑥 ∈ No ↦ dom 𝑥)
7	1, 6	wceq 1475	1 wff bday = (𝑥 ∈ No ↦ dom 𝑥)

This definition is referenced by:  bdayval  31045  bdayfo  31074