Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal numbers - cuts and options
rightirr
Next ⟩
left0s
Metamath Proof Explorer
Ascii
Unicode
Theorem
rightirr
Description:
No surreal is a member of its right set.
(Contributed by
Scott Fenton
, 20-Aug-2024)
Ref
Expression
Assertion
rightirr
⊢
X
∈
No
→
¬
X
∈
R
⁡
X
Proof
Step
Hyp
Ref
Expression
1
oldirr
⊢
¬
X
∈
Old
⁡
bday
⁡
X
2
rightssold
⊢
X
∈
No
→
R
⁡
X
⊆
Old
⁡
bday
⁡
X
3
2
sseld
⊢
X
∈
No
→
X
∈
R
⁡
X
→
X
∈
Old
⁡
bday
⁡
X
4
1
3
mtoi
⊢
X
∈
No
→
¬
X
∈
R
⁡
X