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