Metamath Proof Explorer

Theorem n0p1nns

Description: One plus a non-negative surreal integer is a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025)

Ref Expression
Assertion n0p1nns 
|- ( A e. NN0_s -> ( A +s 1s ) e. NN_s )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = 0s -> ( x +s 1s ) = ( 0s +s 1s ) )
2 1 eleq1d 
 |-  ( x = 0s -> ( ( x +s 1s ) e. NN_s <-> ( 0s +s 1s ) e. NN_s ) )
3 oveq1 
 |-  ( x = y -> ( x +s 1s ) = ( y +s 1s ) )
4 3 eleq1d 
 |-  ( x = y -> ( ( x +s 1s ) e. NN_s <-> ( y +s 1s ) e. NN_s ) )
5 oveq1 
 |-  ( x = ( y +s 1s ) -> ( x +s 1s ) = ( ( y +s 1s ) +s 1s ) )
6 5 eleq1d 
 |-  ( x = ( y +s 1s ) -> ( ( x +s 1s ) e. NN_s <-> ( ( y +s 1s ) +s 1s ) e. NN_s ) )
7 oveq1 
 |-  ( x = A -> ( x +s 1s ) = ( A +s 1s ) )
8 7 eleq1d 
 |-  ( x = A -> ( ( x +s 1s ) e. NN_s <-> ( A +s 1s ) e. NN_s ) )
9 1sno 
 |-  1s e. No
10 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
11 9 10 ax-mp 
 |-  ( 0s +s 1s ) = 1s
12 1nns 
 |-  1s e. NN_s
13 11 12 eqeltri 
 |-  ( 0s +s 1s ) e. NN_s
14 peano2nns 
 |-  ( ( y +s 1s ) e. NN_s -> ( ( y +s 1s ) +s 1s ) e. NN_s )
15 14 a1i 
 |-  ( y e. NN0_s -> ( ( y +s 1s ) e. NN_s -> ( ( y +s 1s ) +s 1s ) e. NN_s ) )
16 2 4 6 8 13 15 n0sind 
 |-  ( A e. NN0_s -> ( A +s 1s ) e. NN_s )