Metamath Proof Explorer


Theorem bdayval

Description: The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011)

Ref Expression
Assertion bdayval A No bday A = dom A

Proof

Step Hyp Ref Expression
1 dmexg A No dom A V
2 dmeq x = A dom x = dom A
3 df-bday bday = x No dom x
4 2 3 fvmptg A No dom A V bday A = dom A
5 1 4 mpdan A No bday A = dom A