Metamath Proof Explorer

Theorem negsbday

Description: Negation of a surreal number preserves birthday. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Assertion negsbday 
|- ( A e. No -> ( bday ` ( -us ` A ) ) = ( bday ` A ) )

Proof

Step Hyp Ref Expression
1 negsbdaylem 
 |-  ( A e. No -> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) )
2 negnegs 
 |-  ( A e. No -> ( -us ` ( -us ` A ) ) = A )
3 2 fveq2d 
 |-  ( A e. No -> ( bday ` ( -us ` ( -us ` A ) ) ) = ( bday ` A ) )
4 negscl 
 |-  ( A e. No -> ( -us ` A ) e. No )
5 negsbdaylem 
 |-  ( ( -us ` A ) e. No -> ( bday ` ( -us ` ( -us ` A ) ) ) C_ ( bday ` ( -us ` A ) ) )
6 4 5 syl 
 |-  ( A e. No -> ( bday ` ( -us ` ( -us ` A ) ) ) C_ ( bday ` ( -us ` A ) ) )
7 3 6 eqsstrrd 
 |-  ( A e. No -> ( bday ` A ) C_ ( bday ` ( -us ` A ) ) )
8 1 7 eqssd 
 |-  ( A e. No -> ( bday ` ( -us ` A ) ) = ( bday ` A ) )