Metamath Proof Explorer

Theorem 1ons

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

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

Proof

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