Metamath Proof Explorer

Theorem nn1m1nns

Description: Every positive surreal integer is either one or a successor. (Contributed by Scott Fenton, 8-Nov-2025)

Ref Expression
Assertion nn1m1nns 
|- ( A e. NN_s -> ( A = 1s \/ ( A -s 1s ) e. NN_s ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( x = 1s -> ( x = 1s <-> 1s = 1s ) )
2 oveq1 
 |-  ( x = 1s -> ( x -s 1s ) = ( 1s -s 1s ) )
3 2 eleq1d 
 |-  ( x = 1s -> ( ( x -s 1s ) e. NN_s <-> ( 1s -s 1s ) e. NN_s ) )
4 1 3 orbi12d 
 |-  ( x = 1s -> ( ( x = 1s \/ ( x -s 1s ) e. NN_s ) <-> ( 1s = 1s \/ ( 1s -s 1s ) e. NN_s ) ) )
5 eqeq1 
 |-  ( x = y -> ( x = 1s <-> y = 1s ) )
6 oveq1 
 |-  ( x = y -> ( x -s 1s ) = ( y -s 1s ) )
7 6 eleq1d 
 |-  ( x = y -> ( ( x -s 1s ) e. NN_s <-> ( y -s 1s ) e. NN_s ) )
8 5 7 orbi12d 
 |-  ( x = y -> ( ( x = 1s \/ ( x -s 1s ) e. NN_s ) <-> ( y = 1s \/ ( y -s 1s ) e. NN_s ) ) )
9 eqeq1 
 |-  ( x = ( y +s 1s ) -> ( x = 1s <-> ( y +s 1s ) = 1s ) )
10 oveq1 
 |-  ( x = ( y +s 1s ) -> ( x -s 1s ) = ( ( y +s 1s ) -s 1s ) )
11 10 eleq1d 
 |-  ( x = ( y +s 1s ) -> ( ( x -s 1s ) e. NN_s <-> ( ( y +s 1s ) -s 1s ) e. NN_s ) )
12 9 11 orbi12d 
 |-  ( x = ( y +s 1s ) -> ( ( x = 1s \/ ( x -s 1s ) e. NN_s ) <-> ( ( y +s 1s ) = 1s \/ ( ( y +s 1s ) -s 1s ) e. NN_s ) ) )
13 eqeq1 
 |-  ( x = A -> ( x = 1s <-> A = 1s ) )
14 oveq1 
 |-  ( x = A -> ( x -s 1s ) = ( A -s 1s ) )
15 14 eleq1d 
 |-  ( x = A -> ( ( x -s 1s ) e. NN_s <-> ( A -s 1s ) e. NN_s ) )
16 13 15 orbi12d 
 |-  ( x = A -> ( ( x = 1s \/ ( x -s 1s ) e. NN_s ) <-> ( A = 1s \/ ( A -s 1s ) e. NN_s ) ) )
17 eqid 
 |-  1s = 1s
18 17 orci 
 |-  ( 1s = 1s \/ ( 1s -s 1s ) e. NN_s )
19 nnsno 
 |-  ( y e. NN_s -> y e. No )
20 1sno 
 |-  1s e. No
21 pncans 
 |-  ( ( y e. No /\ 1s e. No ) -> ( ( y +s 1s ) -s 1s ) = y )
22 19 20 21 sylancl 
 |-  ( y e. NN_s -> ( ( y +s 1s ) -s 1s ) = y )
23 id 
 |-  ( y e. NN_s -> y e. NN_s )
24 22 23 eqeltrd 
 |-  ( y e. NN_s -> ( ( y +s 1s ) -s 1s ) e. NN_s )
25 24 olcd 
 |-  ( y e. NN_s -> ( ( y +s 1s ) = 1s \/ ( ( y +s 1s ) -s 1s ) e. NN_s ) )
26 25 a1d 
 |-  ( y e. NN_s -> ( ( y = 1s \/ ( y -s 1s ) e. NN_s ) -> ( ( y +s 1s ) = 1s \/ ( ( y +s 1s ) -s 1s ) e. NN_s ) ) )
27 4 8 12 16 18 26 nnsind 
 |-  ( A e. NN_s -> ( A = 1s \/ ( A -s 1s ) e. NN_s ) )