Metamath Proof Explorer

Theorem fvnobday

Description: The value of a surreal at its birthday is (/) . (Contributed by Scott Fenton, 14-Jun-2011) (Proof shortened by SF, 14-Apr-2012)

Ref Expression
Assertion fvnobday 
|- ( A e. No -> ( A ` ( bday ` A ) ) = (/) )

Proof

Step Hyp Ref Expression
1 bdayval 
 |-  ( A e. No -> ( bday ` A ) = dom A )
2 nodmord 
 |-  ( A e. No -> Ord dom A )
3 ordirr 
 |-  ( Ord dom A -> -. dom A e. dom A )
4 2 3 syl 
 |-  ( A e. No -> -. dom A e. dom A )
5 1 4 eqneltrd 
 |-  ( A e. No -> -. ( bday ` A ) e. dom A )
6 ndmfv 
 |-  ( -. ( bday ` A ) e. dom A -> ( A ` ( bday ` A ) ) = (/) )
7 5 6 syl 
 |-  ( A e. No -> ( A ` ( bday ` A ) ) = (/) )