Metamath Proof Explorer

Theorem 0ons

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

Ref Expression
Assertion 0ons 
|- 0s e. On_s

Proof

Step Hyp Ref Expression
1 0sno 
 |-  0s e. No
2 right0s 
 |-  ( _Right ` 0s ) = (/)
3 elons 
 |-  ( 0s e. On_s <-> ( 0s e. No /\ ( _Right ` 0s ) = (/) ) )
4 1 2 3 mpbir2an 
 |-  0s e. On_s