Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal numbers - cuts and options
rightval
Next ⟩
leftf
Metamath Proof Explorer
Ascii
Unicode
Theorem
rightval
Description:
The value of the right options function.
(Contributed by
Scott Fenton
, 6-Aug-2024)
Ref
Expression
Assertion
rightval
⊢
A
∈
No
→
R
⁡
A
=
x
∈
Old
⁡
bday
⁡
A
|
A
<
s
x
Proof
Step
Hyp
Ref
Expression
1
2fveq3
⊢
y
=
A
→
Old
⁡
bday
⁡
y
=
Old
⁡
bday
⁡
A
2
breq1
⊢
y
=
A
→
y
<
s
x
↔
A
<
s
x
3
1
2
rabeqbidv
⊢
y
=
A
→
x
∈
Old
⁡
bday
⁡
y
|
y
<
s
x
=
x
∈
Old
⁡
bday
⁡
A
|
A
<
s
x
4
df-right
⊢
R
=
y
∈
No
⟼
x
∈
Old
⁡
bday
⁡
y
|
y
<
s
x
5
fvex
⊢
Old
⁡
bday
⁡
A
∈
V
6
5
rabex
⊢
x
∈
Old
⁡
bday
⁡
A
|
A
<
s
x
∈
V
7
3
4
6
fvmpt
⊢
A
∈
No
→
R
⁡
A
=
x
∈
Old
⁡
bday
⁡
A
|
A
<
s
x