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		0elon	$$⊢\varnothing \in \mathrm{On}$$
2		newval	$$⊢\varnothing \in \mathrm{On}\to N\left(\varnothing \right)=M\left(\varnothing \right)\setminus \mathrm{Old}\left(\varnothing \right)$$
3	1 2	ax-mp	$$⊢N\left(\varnothing \right)=M\left(\varnothing \right)\setminus \mathrm{Old}\left(\varnothing \right)$$
4		made0	Could not format ( _M ` (/) ) = { 0s } : No typesetting found for |- ( _M ` (/) ) = { 0s } with typecode |-
5		old0	$$⊢\mathrm{Old}\left(\varnothing \right)=\varnothing$$
6	4 5	difeq12i	Could not format ( ( _M ` (/) ) \ ( _Old ` (/) ) ) = ( { 0s } \ (/) ) : No typesetting found for |- ( ( _M ` (/) ) \ ( _Old ` (/) ) ) = ( { 0s } \ (/) ) with typecode |-
7		dif0	Could not format ( { 0s } \ (/) ) = { 0s } : No typesetting found for |- ( { 0s } \ (/) ) = { 0s } with typecode |-
8	3 6 7	3eqtri	Could not format ( _N ` (/) ) = { 0s } : No typesetting found for |- ( _N ` (/) ) = { 0s } with typecode |-