Metamath Proof Explorer


Definition df-made

Description: Define the made by function. This function carries an ordinal to all surreals made by sections of surreals older than it. Definition from Conway p. 29. (Contributed by Scott Fenton, 17-Dec-2021)

Ref Expression
Assertion df-made
|- _M = recs ( ( f e. _V |-> ( |s " ( ~P U. ran f X. ~P U. ran f ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmade
 |-  _M
1 vf
 |-  f
2 cvv
 |-  _V
3 cscut
 |-  |s
4 1 cv
 |-  f
5 4 crn
 |-  ran f
6 5 cuni
 |-  U. ran f
7 6 cpw
 |-  ~P U. ran f
8 7 7 cxp
 |-  ( ~P U. ran f X. ~P U. ran f )
9 3 8 cima
 |-  ( |s " ( ~P U. ran f X. ~P U. ran f ) )
10 1 2 9 cmpt
 |-  ( f e. _V |-> ( |s " ( ~P U. ran f X. ~P U. ran f ) ) )
11 10 crecs
 |-  recs ( ( f e. _V |-> ( |s " ( ~P U. ran f X. ~P U. ran f ) ) ) )
12 0 11 wceq
 |-  _M = recs ( ( f e. _V |-> ( |s " ( ~P U. ran f X. ~P U. ran f ) ) ) )