Metamath Proof Explorer


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 cslt <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 𝑦 } )