Theorem negsbday

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

	Ref	Expression
Assertion	negsbday	Could not format assertion : No typesetting found for |- ( A e. No -> ( bday ` ( -us ` A ) ) = ( bday ` A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		negsbdaylem	Could not format ( A e. No -> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) ) : No typesetting found for |- ( A e. No -> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) ) with typecode |-
2		negnegs	Could not format ( A e. No -> ( -us ` ( -us ` A ) ) = A ) : No typesetting found for |- ( A e. No -> ( -us ` ( -us ` A ) ) = A ) with typecode |-
3	2	fveq2d	Could not format ( A e. No -> ( bday ` ( -us ` ( -us ` A ) ) ) = ( bday ` A ) ) : No typesetting found for |- ( A e. No -> ( bday ` ( -us ` ( -us ` A ) ) ) = ( bday ` A ) ) with typecode |-
4		negscl	Could not format ( A e. No -> ( -us ` A ) e. No ) : No typesetting found for |- ( A e. No -> ( -us ` A ) e. No ) with typecode |-
5		negsbdaylem	Could not format ( ( -us ` A ) e. No -> ( bday ` ( -us ` ( -us ` A ) ) ) C_ ( bday ` ( -us ` A ) ) ) : No typesetting found for |- ( ( -us ` A ) e. No -> ( bday ` ( -us ` ( -us ` A ) ) ) C_ ( bday ` ( -us ` A ) ) ) with typecode |-
6	4 5	syl	Could not format ( A e. No -> ( bday ` ( -us ` ( -us ` A ) ) ) C_ ( bday ` ( -us ` A ) ) ) : No typesetting found for |- ( A e. No -> ( bday ` ( -us ` ( -us ` A ) ) ) C_ ( bday ` ( -us ` A ) ) ) with typecode |-
7	3 6	eqsstrrd	Could not format ( A e. No -> ( bday ` A ) C_ ( bday ` ( -us ` A ) ) ) : No typesetting found for |- ( A e. No -> ( bday ` A ) C_ ( bday ` ( -us ` A ) ) ) with typecode |-
8	1 7	eqssd	Could not format ( A e. No -> ( bday ` ( -us ` A ) ) = ( bday ` A ) ) : No typesetting found for |- ( A e. No -> ( bday ` ( -us ` A ) ) = ( bday ` A ) ) with typecode |-