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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cold	$$class\mathrm{Old}$$
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	3 4	cima	Could not format ( _Made " x ) : No typesetting found for class ( _Made " x ) with typecode class
6	5	cuni	Could not format U. ( _Made " x ) : No typesetting found for class U. ( _Made " x ) with typecode class
7	1 2 6	cmpt	Could not format ( x e. On |-> U. ( _Made " x ) ) : No typesetting found for class ( x e. On |-> U. ( _Made " x ) ) with typecode class
8	0 7	wceq	Could not format _Old = ( x e. On |-> U. ( _Made " x ) ) : No typesetting found for wff _Old = ( x e. On |-> U. ( _Made " x ) ) with typecode wff