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	Could not format assertion : No typesetting found for |- _Made = recs ( ( f e. _V |-> ( |s " ( ~P U. ran f X. ~P U. ran f ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmade	Could not format _Made : No typesetting found for class _Made with typecode class
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		cscut	$$class{|}_s$$
4	1	cv	$$setvarf$$
5	4	crn	$$class\mathrm{ran}f$$
6	5	cuni	$$class\bigcup \mathrm{ran}f$$
7	6	cpw	$$class𝒫\bigcup \mathrm{ran}f$$
8	7 7	cxp	$$class\left(𝒫\bigcup \mathrm{ran}f\times 𝒫\bigcup \mathrm{ran}f\right)$$
9	3 8	cima	$$class{|}_s\left[𝒫\bigcup \mathrm{ran}f\times 𝒫\bigcup \mathrm{ran}f\right]$$
10	1 2 9	cmpt	$$class\left(f\in \mathrm{V}⟼{|}_s\left[𝒫\bigcup \mathrm{ran}f\times 𝒫\bigcup \mathrm{ran}f\right]\right)$$
11	10	crecs	$$class\mathrm{recs}\left(\left(f\in \mathrm{V}⟼{|}_s\left[𝒫\bigcup \mathrm{ran}f\times 𝒫\bigcup \mathrm{ran}f\right]\right)\right)$$
12	0 11	wceq	Could not format _Made = recs ( ( f e. _V |-> ( |s " ( ~P U. ran f X. ~P U. ran f ) ) ) ) : No typesetting found for wff _Made = recs ( ( f e. _V |-> ( |s " ( ~P U. ran f X. ~P U. ran f ) ) ) ) with typecode wff