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	⊢ O = ( 𝑥 ∈ On ↦ ∪ ( M “ 𝑥 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cold	⊢ O
1		vx	⊢ 𝑥
2		con0	⊢ On
3		cmade	⊢ M
4	1	cv	⊢ 𝑥
5	3 4	cima	⊢ ( M “ 𝑥 )
6	5	cuni	⊢ ∪ ( M “ 𝑥 )
7	1 2 6	cmpt	⊢ ( 𝑥 ∈ On ↦ ∪ ( M “ 𝑥 ) )
8	0 7	wceq	⊢ O = ( 𝑥 ∈ On ↦ ∪ ( M “ 𝑥 ) )