Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal numbers - cuts and options
leftssold
Next ⟩
rightssold
Metamath Proof Explorer
Ascii
Unicode
Theorem
leftssold
Description:
The left options are a subset of the old set.
(Contributed by
Scott Fenton
, 9-Oct-2024)
Ref
Expression
Assertion
leftssold
⊢
L
⁡
X
⊆
Old
⁡
bday
⁡
X
Proof
Step
Hyp
Ref
Expression
1
leftval
⊢
L
⁡
X
=
x
∈
Old
⁡
bday
⁡
X
|
x
<
s
X
2
ssrab2
⊢
x
∈
Old
⁡
bday
⁡
X
|
x
<
s
X
⊆
Old
⁡
bday
⁡
X
3
1
2
eqsstri
⊢
L
⁡
X
⊆
Old
⁡
bday
⁡
X