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	$$⊢\mathrm{Old}=\left(x\in \mathrm{On}⟼\bigcup M\left[x\right]\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cold	$$class\mathrm{Old}$$
1		vx	$$setvarx$$
2		con0	$$class\mathrm{On}$$
3		cmade	$$classM$$
4	1	cv	$$setvarx$$
5	3 4	cima	$$classM\left[x\right]$$
6	5	cuni	$$class\bigcup M\left[x\right]$$
7	1 2 6	cmpt	$$class\left(x\in \mathrm{On}⟼\bigcup M\left[x\right]\right)$$
8	0 7	wceq	$$wff\mathrm{Old}=\left(x\in \mathrm{On}⟼\bigcup M\left[x\right]\right)$$