Database
SURREAL NUMBERS
Subsystems of surreals
Integers
zno
Next ⟩
znod
Metamath Proof Explorer
Ascii
Structured
Theorem
zno
Description:
A surreal integer is a surreal.
(Contributed by
Scott Fenton
, 17-May-2025)
Ref
Expression
Assertion
zno
⊢
(
𝐴
∈ ℤ
s
→
𝐴
∈
No
)
Proof
Step
Hyp
Ref
Expression
1
zssno
⊢
ℤ
s
⊆
No
2
1
sseli
⊢
(
𝐴
∈ ℤ
s
→
𝐴
∈
No
)