Description: Define the newer than function. This function carries an ordinal to all surreals made on that day. Definition from Conway p. 29. (Contributed by Scott Fenton, 17-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-new | |- _N = ( x e. On |-> ( ( _M ` x ) \ ( _Old ` x ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cnew | |- _N |
|
| 1 | vx | |- x |
|
| 2 | con0 | |- On |
|
| 3 | cmade | |- _M |
|
| 4 | 1 | cv | |- x |
| 5 | 4 3 | cfv | |- ( _M ` x ) |
| 6 | cold | |- _Old |
|
| 7 | 4 6 | cfv | |- ( _Old ` x ) |
| 8 | 5 7 | cdif | |- ( ( _M ` x ) \ ( _Old ` x ) ) |
| 9 | 1 2 8 | cmpt | |- ( x e. On |-> ( ( _M ` x ) \ ( _Old ` x ) ) ) |
| 10 | 0 9 | wceq | |- _N = ( x e. On |-> ( ( _M ` x ) \ ( _Old ` x ) ) ) |