Database
SURREAL NUMBERS
Conway cut representation
Cuts and Options
newno
Next ⟩
madenod
Metamath Proof Explorer
Ascii
Unicode
Theorem
newno
Description:
An element of a new set is a surreal.
(Contributed by
Scott Fenton
, 27-Feb-2026)
Ref
Expression
Assertion
newno
⊢
A
∈
N
⁡
B
→
A
∈
No
Proof
Step
Hyp
Ref
Expression
1
newssno
⊢
N
⁡
B
⊆
No
2
1
sseli
⊢
A
∈
N
⁡
B
→
A
∈
No