Metamath Proof Explorer

Theorem peano2ons

Description: The successor of a surreal ordinal is a surreal ordinal. (Contributed by Scott Fenton, 22-Aug-2025)

Ref Expression
Assertion peano2ons 
|- ( A e. On_s -> ( A +s 1s ) e. On_s )

Proof

Step Hyp Ref Expression
1 1ons 
 |-  1s e. On_s
2 onaddscl 
 |-  ( ( A e. On_s /\ 1s e. On_s ) -> ( A +s 1s ) e. On_s )
3 1 2 mpan2 
 |-  ( A e. On_s -> ( A +s 1s ) e. On_s )