Theorem 0ons

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

	Ref	Expression
Assertion	0ons	$$⊢0_s\in {On}_s$$

Proof

Step	Hyp	Ref	Expression
1		0sno	$$⊢0_s\in \mathrm{No}$$
2		right0s	$$⊢R\left(0_s\right)=\varnothing$$
3		elons	$$⊢0_s\in {On}_s\leftrightarrow \left(0_s\in \mathrm{No}\wedge R\left(0_s\right)=\varnothing \right)$$
4	1 2 3	mpbir2an	$$⊢0_s\in {On}_s$$