Metamath Proof Explorer

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