Metamath Proof Explorer

Theorem nofnbday

Description: A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion nofnbday 
|- ( A e. No -> A Fn ( bday ` A ) )

Proof

Step Hyp Ref Expression
1 nofun 
 |-  ( A e. No -> Fun A )
2 bdayval 
 |-  ( A e. No -> ( bday ` A ) = dom A )
3 2 eqcomd 
 |-  ( A e. No -> dom A = ( bday ` A ) )
4 df-fn 
 |-  ( A Fn ( bday ` A ) <-> ( Fun A /\ dom A = ( bday ` A ) ) )
5 1 3 4 sylanbrc 
 |-  ( A e. No -> A Fn ( bday ` A ) )