Theorem new0

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

	Ref	Expression
Assertion	new0	Could not format assertion : No typesetting found for |- ( _N ` (/) ) = { 0s } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		newval	$$⊢N\left(\varnothing \right)=M\left(\varnothing \right)\setminus \mathrm{Old}\left(\varnothing \right)$$
2		made0	Could not format ( _M ` (/) ) = { 0s } : No typesetting found for |- ( _M ` (/) ) = { 0s } with typecode |-
3		old0	$$⊢\mathrm{Old}\left(\varnothing \right)=\varnothing$$
4	2 3	difeq12i	Could not format ( ( _M ` (/) ) \ ( _Old ` (/) ) ) = ( { 0s } \ (/) ) : No typesetting found for |- ( ( _M ` (/) ) \ ( _Old ` (/) ) ) = ( { 0s } \ (/) ) with typecode |-
5		dif0	Could not format ( { 0s } \ (/) ) = { 0s } : No typesetting found for |- ( { 0s } \ (/) ) = { 0s } with typecode |-
6	1 4 5	3eqtri	Could not format ( _N ` (/) ) = { 0s } : No typesetting found for |- ( _N ` (/) ) = { 0s } with typecode |-