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 |- ( _New ` (/) ) = { 0s } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		newval	Could not format ( _New ` (/) ) = ( ( _Made ` (/) ) \ ( _Old ` (/) ) ) : No typesetting found for |- ( _New ` (/) ) = ( ( _Made ` (/) ) \ ( _Old ` (/) ) ) with typecode |-
2		made0	Could not format ( _Made ` (/) ) = { 0s } : No typesetting found for |- ( _Made ` (/) ) = { 0s } with typecode |-
3		old0	$$⊢\mathrm{Old}\left(\varnothing \right)=\varnothing$$
4	2 3	difeq12i	Could not format ( ( _Made ` (/) ) \ ( _Old ` (/) ) ) = ( { 0s } \ (/) ) : No typesetting found for |- ( ( _Made ` (/) ) \ ( _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 ( _New ` (/) ) = { 0s } : No typesetting found for |- ( _New ` (/) ) = { 0s } with typecode |-