Database
SURREAL NUMBERS
Conway cut representation
Cuts and Options
rightno
Next ⟩
leftoldd
Metamath Proof Explorer
Ascii
Structured
Theorem
rightno
Description:
An element of a right set is a surreal.
(Contributed by
Scott Fenton
, 27-Feb-2026)
Ref
Expression
Assertion
rightno
⊢
(
𝐴
∈ ( R ‘
𝐵
) →
𝐴
∈
No
)
Proof
Step
Hyp
Ref
Expression
1
rightssno
⊢
( R ‘
𝐵
) ⊆
No
2
1
sseli
⊢
(
𝐴
∈ ( R ‘
𝐵
) →
𝐴
∈
No
)