Definition df-bday

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
Assertion	df-bday	⊢ bday = ( 𝑥 ∈ No ↦ dom 𝑥 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbday	⊢ bday
1		vx	⊢ 𝑥
2		csur	⊢ No
3	1	cv	⊢ 𝑥
4	3	cdm	⊢ dom 𝑥
5	1 2 4	cmpt	⊢ ( 𝑥 ∈ No ↦ dom 𝑥 )
6	0 5	wceq	⊢ bday = ( 𝑥 ∈ No ↦ dom 𝑥 )