Metamath Proof Explorer

Theorem n0s0m1

Description: Every non-negative surreal integer is either zero or a successor. (Contributed by Scott Fenton, 26-May-2025)

Ref Expression
Assertion n0s0m1 
|- ( A e. NN0_s -> ( A = 0s \/ ( A -s 1s ) e. NN0_s ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( x = 0s -> ( x = 0s <-> 0s = 0s ) )
2 oveq1 
 |-  ( x = 0s -> ( x -s 1s ) = ( 0s -s 1s ) )
3 2 eleq1d 
 |-  ( x = 0s -> ( ( x -s 1s ) e. NN0_s <-> ( 0s -s 1s ) e. NN0_s ) )
4 1 3 orbi12d 
 |-  ( x = 0s -> ( ( x = 0s \/ ( x -s 1s ) e. NN0_s ) <-> ( 0s = 0s \/ ( 0s -s 1s ) e. NN0_s ) ) )
5 eqeq1 
 |-  ( x = y -> ( x = 0s <-> y = 0s ) )
6 oveq1 
 |-  ( x = y -> ( x -s 1s ) = ( y -s 1s ) )
7 6 eleq1d 
 |-  ( x = y -> ( ( x -s 1s ) e. NN0_s <-> ( y -s 1s ) e. NN0_s ) )
8 5 7 orbi12d 
 |-  ( x = y -> ( ( x = 0s \/ ( x -s 1s ) e. NN0_s ) <-> ( y = 0s \/ ( y -s 1s ) e. NN0_s ) ) )
9 eqeq1 
 |-  ( x = ( y +s 1s ) -> ( x = 0s <-> ( y +s 1s ) = 0s ) )
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. NN0_s <-> ( ( y +s 1s ) -s 1s ) e. NN0_s ) )
12 9 11 orbi12d 
 |-  ( x = ( y +s 1s ) -> ( ( x = 0s \/ ( x -s 1s ) e. NN0_s ) <-> ( ( y +s 1s ) = 0s \/ ( ( y +s 1s ) -s 1s ) e. NN0_s ) ) )
13 eqeq1 
 |-  ( x = A -> ( x = 0s <-> A = 0s ) )
14 oveq1 
 |-  ( x = A -> ( x -s 1s ) = ( A -s 1s ) )
15 14 eleq1d 
 |-  ( x = A -> ( ( x -s 1s ) e. NN0_s <-> ( A -s 1s ) e. NN0_s ) )
16 13 15 orbi12d 
 |-  ( x = A -> ( ( x = 0s \/ ( x -s 1s ) e. NN0_s ) <-> ( A = 0s \/ ( A -s 1s ) e. NN0_s ) ) )
17 eqid 
 |-  0s = 0s
18 17 orci 
 |-  ( 0s = 0s \/ ( 0s -s 1s ) e. NN0_s )
19 n0sno 
 |-  ( y e. NN0_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. NN0_s -> ( ( y +s 1s ) -s 1s ) = y )
23 id 
 |-  ( y e. NN0_s -> y e. NN0_s )
24 22 23 eqeltrd 
 |-  ( y e. NN0_s -> ( ( y +s 1s ) -s 1s ) e. NN0_s )
25 24 olcd 
 |-  ( y e. NN0_s -> ( ( y +s 1s ) = 0s \/ ( ( y +s 1s ) -s 1s ) e. NN0_s ) )
26 25 a1d 
 |-  ( y e. NN0_s -> ( ( y = 0s \/ ( y -s 1s ) e. NN0_s ) -> ( ( y +s 1s ) = 0s \/ ( ( y +s 1s ) -s 1s ) e. NN0_s ) ) )
27 4 8 12 16 18 26 n0sind 
 |-  ( A e. NN0_s -> ( A = 0s \/ ( A -s 1s ) e. NN0_s ) )