Metamath Proof Explorer

Theorem peano2no

Description: A theorem for surreals that is analogous to the second Peano postulate peano2 . (Contributed by Scott Fenton, 17-Mar-2025)

Ref Expression
Assertion peano2no 
|- ( A e. No -> ( A +s 1s ) e. No )

Proof

Step Hyp Ref Expression
1 1sno 
 |-  1s e. No
2 addscl 
 |-  ( ( A e. No /\ 1s e. No ) -> ( A +s 1s ) e. No )
3 1 2 mpan2 
 |-  ( A e. No -> ( A +s 1s ) e. No )