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 = ( 𝑥 ∈ On ↦ ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnew	⊢ N
1		vx	⊢ 𝑥
2		con0	⊢ On
3		cmade	⊢ M
4	1	cv	⊢ 𝑥
5	4 3	cfv	⊢ ( M ‘ 𝑥 )
6		cold	⊢ O
7	4 6	cfv	⊢ ( O ‘ 𝑥 )
8	5 7	cdif	⊢ ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) )
9	1 2 8	cmpt	⊢ ( 𝑥 ∈ On ↦ ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) )
10	0 9	wceq	⊢ N = ( 𝑥 ∈ On ↦ ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) )