Database
SURREAL NUMBERS
Subsystems of surreals
Natural numbers
n0sno
Next ⟩
nnsno
Metamath Proof Explorer
Ascii
Structured
Theorem
n0sno
Description:
A non-negative surreal integer is a surreal.
(Contributed by
Scott Fenton
, 15-Apr-2025)
Ref
Expression
Assertion
n0sno
⊢
(
𝐴
∈ ℕ
0s
→
𝐴
∈
No
)
Proof
Step
Hyp
Ref
Expression
1
n0ssno
⊢
ℕ
0s
⊆
No
2
1
sseli
⊢
(
𝐴
∈ ℕ
0s
→
𝐴
∈
No
)