Definition df-new

Description: Define the newer than function. This function carries an ordinal to all surreals made on that day. Definition from Conway p. 29. (Contributed by Scott Fenton, 17-Dec-2021)

	Ref	Expression
Assertion	df-new	$$⊢N=\left(x\in \mathrm{On}⟼M\left(x\right)\setminus \mathrm{Old}\left(x\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnew	$$classN$$
1		vx	$$setvarx$$
2		con0	$$class\mathrm{On}$$
3		cmade	$$classM$$
4	1	cv	$$setvarx$$
5	4 3	cfv	$$classM\left(x\right)$$
6		cold	$$class\mathrm{Old}$$
7	4 6	cfv	$$class\mathrm{Old}\left(x\right)$$
8	5 7	cdif	$$class\left(M\left(x\right)\setminus \mathrm{Old}\left(x\right)\right)$$
9	1 2 8	cmpt	$$class\left(x\in \mathrm{On}⟼M\left(x\right)\setminus \mathrm{Old}\left(x\right)\right)$$
10	0 9	wceq	$$wffN=\left(x\in \mathrm{On}⟼M\left(x\right)\setminus \mathrm{Old}\left(x\right)\right)$$