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	Could not format assertion : No typesetting found for |- _New = ( x e. On |-> ( ( _Made ` x ) \ ( _Old ` x ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnew	Could not format _New : No typesetting found for class _New with typecode class
1		vx	$$setvarx$$
2		con0	$$class\mathrm{On}$$
3		cmade	Could not format _Made : No typesetting found for class _Made with typecode class
4	1	cv	$$setvarx$$
5	4 3	cfv	Could not format ( _Made ` x ) : No typesetting found for class ( _Made ` x ) with typecode class
6		cold	$$class\mathrm{Old}$$
7	4 6	cfv	$$class\mathrm{Old}\left(x\right)$$
8	5 7	cdif	Could not format ( ( _Made ` x ) \ ( _Old ` x ) ) : No typesetting found for class ( ( _Made ` x ) \ ( _Old ` x ) ) with typecode class
9	1 2 8	cmpt	Could not format ( x e. On |-> ( ( _Made ` x ) \ ( _Old ` x ) ) ) : No typesetting found for class ( x e. On |-> ( ( _Made ` x ) \ ( _Old ` x ) ) ) with typecode class
10	0 9	wceq	Could not format _New = ( x e. On |-> ( ( _Made ` x ) \ ( _Old ` x ) ) ) : No typesetting found for wff _New = ( x e. On |-> ( ( _Made ` x ) \ ( _Old ` x ) ) ) with typecode wff