Metamath Proof Explorer


Theorem onno

Description: A surreal ordinal is a surreal. (Contributed by Scott Fenton, 18-Mar-2025)

Ref Expression
Assertion onno ( 𝐴 ∈ Ons → 𝐴 ∈ No )

Proof

Step Hyp Ref Expression
1 onssno ⊢ Ons ⊆ No
2 1 sseli ⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )