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 e. No -> ( bday ` A ) = dom A )

Proof

Step Hyp Ref Expression
1 dmexg 
 |-  ( A e. No -> dom A e. _V )
2 dmeq 
 |-  ( x = A -> dom x = dom A )
3 df-bday 
 |-  bday = ( x e. No |-> dom x )
4 2 3 fvmptg 
 |-  ( ( A e. No /\ dom A e. _V ) -> ( bday ` A ) = dom A )
5 1 4 mpdan 
 |-  ( A e. No -> ( bday ` A ) = dom A )