Definition df-right

Description: Define the right options of a surreal. This is the set of surreals that are simpler and greater than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024)

	Ref	Expression
Assertion	df-right	⊢ R = ( 𝑥 ∈ No ↦ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cright	⊢ R
1		vx	⊢ 𝑥
2		csur	⊢ No
3		vy	⊢ 𝑦
4		cold	⊢ O
5		cbday	⊢ bday
6	1	cv	⊢ 𝑥
7	6 5	cfv	⊢ ( bday ‘ 𝑥 )
8	7 4	cfv	⊢ ( O ‘ ( bday ‘ 𝑥 ) )
9		clts	⊢ <s
10	3	cv	⊢ 𝑦
11	6 10 9	wbr	⊢ 𝑥 <s 𝑦
12	11 3 8	crab	⊢ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 }
13	1 2 12	cmpt	⊢ ( 𝑥 ∈ No ↦ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 } )
14	0 13	wceq	⊢ R = ( 𝑥 ∈ No ↦ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑥 <s 𝑦 } )