Theorem onno 28518

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

Assertion

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

Proof of Theorem onno

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   No csur 27874  On_scons 28514

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3919  df-ons 28515

This theorem is used by:  elons2  28521  ltonold  28524  oncutleft  28526  oncutlt  28527  onnolt  28529  onlts  28530  onles  28531  bdayons  28539  onaddscl  28540  onmulscl  28541  addonbday  28542  onsbnd2  28545  onsfi  28619