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	|- (/) e. On
2		newval	|- ( (/) e. On -> ( _N ` (/) ) = ( ( _M ` (/) ) \ ( _Old ` (/) ) ) )
3	1 2	ax-mp	|- ( _N ` (/) ) = ( ( _M ` (/) ) \ ( _Old ` (/) ) )
4		made0	|- ( _M ` (/) ) = { 0s }
5		old0	|- ( _Old ` (/) ) = (/)
6	4 5	difeq12i	|- ( ( _M ` (/) ) \ ( _Old ` (/) ) ) = ( { 0s } \ (/) )
7		dif0	|- ( { 0s } \ (/) ) = { 0s }
8	3 6 7	3eqtri	|- ( _N ` (/) ) = { 0s }