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=\mathrm{recs}\left(\left(f\in \mathrm{V}⟼{|}_s\left[𝒫\bigcup \mathrm{ran}f\times 𝒫\bigcup \mathrm{ran}f\right]\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmade	$$classM$$
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	$$wffM=\mathrm{recs}\left(\left(f\in \mathrm{V}⟼{|}_s\left[𝒫\bigcup \mathrm{ran}f\times 𝒫\bigcup \mathrm{ran}f\right]\right)\right)$$