Metamath Proof Explorer


Definition df-old

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 ) )

Detailed syntax breakdown

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 ) )