Theorem new0

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

	Ref	Expression
Assertion	new0	$$⊢N\left(\varnothing \right)=\left\{0_s\right\}$$

Proof

Step	Hyp	Ref	Expression
1		newval	$$⊢N\left(\varnothing \right)=M\left(\varnothing \right)\setminus \mathrm{Old}\left(\varnothing \right)$$
2		made0	$$⊢M\left(\varnothing \right)=\left\{0_s\right\}$$
3		old0	$$⊢\mathrm{Old}\left(\varnothing \right)=\varnothing$$
4	2 3	difeq12i	$$⊢M\left(\varnothing \right)\setminus \mathrm{Old}\left(\varnothing \right)=\left\{0_s\right\}\setminus \varnothing$$
5		dif0	$$⊢\left\{0_s\right\}\setminus \varnothing =\left\{0_s\right\}$$
6	1 4 5	3eqtri	$$⊢N\left(\varnothing \right)=\left\{0_s\right\}$$