Metamath Proof Explorer


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 )