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		0elon	⊢ ∅ ∈ On
2		newval	⊢ ( ∅ ∈ On → ( N ‘ ∅ ) = ( ( M ‘ ∅ ) ∖ ( O ‘ ∅ ) ) )
3	1 2	ax-mp	⊢ ( N ‘ ∅ ) = ( ( M ‘ ∅ ) ∖ ( O ‘ ∅ ) )
4		made0	⊢ ( M ‘ ∅ ) = { 0s }
5		old0	⊢ ( O ‘ ∅ ) = ∅
6	4 5	difeq12i	⊢ ( ( M ‘ ∅ ) ∖ ( O ‘ ∅ ) ) = ( { 0s } ∖ ∅ )
7		dif0	⊢ ( { 0s } ∖ ∅ ) = { 0s }
8	3 6 7	3eqtri	⊢ ( N ‘ ∅ ) = { 0s }