Theorem 0ons

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

	Ref	Expression
Assertion	0ons	⊢ 0s ∈ Ons

Proof

Step	Hyp	Ref	Expression
1		0no	⊢ 0s ∈ No
2		right0s	⊢ ( R ‘ 0s ) = ∅
3		elons	⊢ ( 0s ∈ Ons ↔ ( 0s ∈ No ∧ ( R ‘ 0s ) = ∅ ) )
4	1 2 3	mpbir2an	⊢ 0s ∈ Ons