Theorem negbday

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

	Ref	Expression
Assertion	negbday	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ 𝐴 ) ) = ( bday ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		negbdaylem	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ 𝐴 ) ) ⊆ ( bday ‘ 𝐴 ) )
2		negnegs	⊢ ( 𝐴 ∈ No → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
3	2	fveq2d	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ ( -us ‘ 𝐴 ) ) ) = ( bday ‘ 𝐴 ) )
4		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
5		negbdaylem	⊢ ( ( -us ‘ 𝐴 ) ∈ No → ( bday ‘ ( -us ‘ ( -us ‘ 𝐴 ) ) ) ⊆ ( bday ‘ ( -us ‘ 𝐴 ) ) )
6	4 5	syl	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ ( -us ‘ 𝐴 ) ) ) ⊆ ( bday ‘ ( -us ‘ 𝐴 ) ) )
7	3 6	eqsstrrd	⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) ⊆ ( bday ‘ ( -us ‘ 𝐴 ) ) )
8	1 7	eqssd	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ 𝐴 ) ) = ( bday ‘ 𝐴 ) )