Theorem 0ons

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

	Ref	Expression
Assertion	0ons	Could not format assertion : No typesetting found for |- 0s e. On_s with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
2		right0s	Could not format ( _Right ` 0s ) = (/) : No typesetting found for |- ( _Right ` 0s ) = (/) with typecode |-
3		elons	Could not format ( 0s e. On_s <-> ( 0s e. No /\ ( _Right ` 0s ) = (/) ) ) : No typesetting found for |- ( 0s e. On_s <-> ( 0s e. No /\ ( _Right ` 0s ) = (/) ) ) with typecode |-
4	1 2 3	mpbir2an	Could not format 0s e. On_s : No typesetting found for |- 0s e. On_s with typecode |-