Theorem onssno

Description: The surreal ordinals are a subclass of the surreals. (Contributed by Scott Fenton, 18-Mar-2025)

	Ref	Expression
Assertion	onssno	$$⊢{On}_s\subseteq \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		df-ons	$$⊢{On}_s=\left\{x\in \mathrm{No}|R\left(x\right)=\varnothing \right\}$$
2		ssrab2	$$⊢\left\{x\in \mathrm{No}|R\left(x\right)=\varnothing \right\}\subseteq \mathrm{No}$$
3	1 2	eqsstri	$$⊢{On}_s\subseteq \mathrm{No}$$