Description: Define the older than function. This function carries an ordinal to all surreals made by a previous ordinal. Definition from Conway p. 29. (Contributed by Scott Fenton, 17-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | df-old | |- _Old = ( x e. On |-> U. ( _M " x ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cold | |- _Old |
|
1 | vx | |- x |
|
2 | con0 | |- On |
|
3 | cmade | |- _M |
|
4 | 1 | cv | |- x |
5 | 3 4 | cima | |- ( _M " x ) |
6 | 5 | cuni | |- U. ( _M " x ) |
7 | 1 2 6 | cmpt | |- ( x e. On |-> U. ( _M " x ) ) |
8 | 0 7 | wceq | |- _Old = ( x e. On |-> U. ( _M " x ) ) |