Theorem negbday

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

	Ref	Expression
Assertion	negbday	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(A\right)\right)=\mathrm{bday}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		negbdaylem	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(A\right)\right)\subseteq \mathrm{bday}\left(A\right)$$
2		negnegs	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)=A$$
3	2	fveq2d	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left({+}_s\left(A\right)\right)\right)=\mathrm{bday}\left(A\right)$$
4		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
5		negbdaylem	$$⊢{+}_s\left(A\right)\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left({+}_s\left(A\right)\right)\right)\subseteq \mathrm{bday}\left({+}_s\left(A\right)\right)$$
6	4 5	syl	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left({+}_s\left(A\right)\right)\right)\subseteq \mathrm{bday}\left({+}_s\left(A\right)\right)$$
7	3 6	eqsstrrd	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left(A\right)\subseteq \mathrm{bday}\left({+}_s\left(A\right)\right)$$
8	1 7	eqssd	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(A\right)\right)=\mathrm{bday}\left(A\right)$$