Definition df-right 27839

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.)

Assertion

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

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-right

Step	Hyp	Ref	Expression
1		cright 27834	. 2 class R
2		vx	. . 3 setvar 𝑥
3		csur 27619	. . 3 class No
4	2	cv 1541	. . . . 5 class 𝑥
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1541	. . . . 5 class 𝑦
7		clts 27620	. . . . 5 class <s
8	4, 6, 7	wbr 5100	. . . 4 wff 𝑥 <s 𝑦
9		cbday 27621	. . . . . 6 class bday
10	4, 9	cfv 6500	. . . . 5 class ( bday ‘𝑥)
11		cold 27831	. . . . 5 class O
12	10, 11	cfv 6500	. . . 4 class ( O ‘( bday ‘𝑥))
13	8, 5, 12	crab 3401	. . 3 class {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑥 <s 𝑦}
14	2, 3, 13	cmpt 5181	. 2 class (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑥 <s 𝑦})
15	1, 14	wceq 1542	1 wff R = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑥 <s 𝑦})

This definition is referenced by:  rightval  27858  rightf  27864