Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal numbers - cuts and options
df-right
Metamath Proof Explorer
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 𝑦 } )