Theorem new0

Description: The only surreal new on day (/) is 0s . (Contributed by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Assertion	new0	⊢ ( N ‘ ∅ ) = { 0s }

Proof

Step	Hyp	Ref	Expression
1		newval	⊢ ( N ‘ ∅ ) = ( ( M ‘ ∅ ) ∖ ( O ‘ ∅ ) )
2		made0	⊢ ( M ‘ ∅ ) = { 0s }
3		old0	⊢ ( O ‘ ∅ ) = ∅
4	2 3	difeq12i	⊢ ( ( M ‘ ∅ ) ∖ ( O ‘ ∅ ) ) = ( { 0s } ∖ ∅ )
5		dif0	⊢ ( { 0s } ∖ ∅ ) = { 0s }
6	1 4 5	3eqtri	⊢ ( N ‘ ∅ ) = { 0s }