Metamath Proof Explorer

Theorem n0s0suc

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

Ref Expression
Assertion n0s0suc 
|- ( A e. NN0_s -> ( A = 0s \/ E. x e. NN0_s A = ( x +s 1s ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( y = 0s -> ( y = 0s <-> 0s = 0s ) )
2 eqeq1 
 |-  ( y = 0s -> ( y = ( x +s 1s ) <-> 0s = ( x +s 1s ) ) )
3 2 rexbidv 
 |-  ( y = 0s -> ( E. x e. NN0_s y = ( x +s 1s ) <-> E. x e. NN0_s 0s = ( x +s 1s ) ) )
4 1 3 orbi12d 
 |-  ( y = 0s -> ( ( y = 0s \/ E. x e. NN0_s y = ( x +s 1s ) ) <-> ( 0s = 0s \/ E. x e. NN0_s 0s = ( x +s 1s ) ) ) )
5 eqeq1 
 |-  ( y = z -> ( y = 0s <-> z = 0s ) )
6 eqeq1 
 |-  ( y = z -> ( y = ( x +s 1s ) <-> z = ( x +s 1s ) ) )
7 6 rexbidv 
 |-  ( y = z -> ( E. x e. NN0_s y = ( x +s 1s ) <-> E. x e. NN0_s z = ( x +s 1s ) ) )
8 5 7 orbi12d 
 |-  ( y = z -> ( ( y = 0s \/ E. x e. NN0_s y = ( x +s 1s ) ) <-> ( z = 0s \/ E. x e. NN0_s z = ( x +s 1s ) ) ) )
9 eqeq1 
 |-  ( y = ( z +s 1s ) -> ( y = 0s <-> ( z +s 1s ) = 0s ) )
10 eqeq1 
 |-  ( y = ( z +s 1s ) -> ( y = ( x +s 1s ) <-> ( z +s 1s ) = ( x +s 1s ) ) )
11 10 rexbidv 
 |-  ( y = ( z +s 1s ) -> ( E. x e. NN0_s y = ( x +s 1s ) <-> E. x e. NN0_s ( z +s 1s ) = ( x +s 1s ) ) )
12 9 11 orbi12d 
 |-  ( y = ( z +s 1s ) -> ( ( y = 0s \/ E. x e. NN0_s y = ( x +s 1s ) ) <-> ( ( z +s 1s ) = 0s \/ E. x e. NN0_s ( z +s 1s ) = ( x +s 1s ) ) ) )
13 eqeq1 
 |-  ( y = A -> ( y = 0s <-> A = 0s ) )
14 eqeq1 
 |-  ( y = A -> ( y = ( x +s 1s ) <-> A = ( x +s 1s ) ) )
15 14 rexbidv 
 |-  ( y = A -> ( E. x e. NN0_s y = ( x +s 1s ) <-> E. x e. NN0_s A = ( x +s 1s ) ) )
16 13 15 orbi12d 
 |-  ( y = A -> ( ( y = 0s \/ E. x e. NN0_s y = ( x +s 1s ) ) <-> ( A = 0s \/ E. x e. NN0_s A = ( x +s 1s ) ) ) )
17 eqid 
 |-  0s = 0s
18 17 orci 
 |-  ( 0s = 0s \/ E. x e. NN0_s 0s = ( x +s 1s ) )
19 clel5 
 |-  ( z e. NN0_s <-> E. x e. NN0_s z = x )
20 19 biimpi 
 |-  ( z e. NN0_s -> E. x e. NN0_s z = x )
21 n0sno 
 |-  ( z e. NN0_s -> z e. No )
22 n0sno 
 |-  ( x e. NN0_s -> x e. No )
23 1sno 
 |-  1s e. No
24 addscan2 
 |-  ( ( z e. No /\ x e. No /\ 1s e. No ) -> ( ( z +s 1s ) = ( x +s 1s ) <-> z = x ) )
25 23 24 mp3an3 
 |-  ( ( z e. No /\ x e. No ) -> ( ( z +s 1s ) = ( x +s 1s ) <-> z = x ) )
26 21 22 25 syl2an 
 |-  ( ( z e. NN0_s /\ x e. NN0_s ) -> ( ( z +s 1s ) = ( x +s 1s ) <-> z = x ) )
27 26 rexbidva 
 |-  ( z e. NN0_s -> ( E. x e. NN0_s ( z +s 1s ) = ( x +s 1s ) <-> E. x e. NN0_s z = x ) )
28 20 27 mpbird 
 |-  ( z e. NN0_s -> E. x e. NN0_s ( z +s 1s ) = ( x +s 1s ) )
29 28 olcd 
 |-  ( z e. NN0_s -> ( ( z +s 1s ) = 0s \/ E. x e. NN0_s ( z +s 1s ) = ( x +s 1s ) ) )
30 29 a1d 
 |-  ( z e. NN0_s -> ( ( z = 0s \/ E. x e. NN0_s z = ( x +s 1s ) ) -> ( ( z +s 1s ) = 0s \/ E. x e. NN0_s ( z +s 1s ) = ( x +s 1s ) ) ) )
31 4 8 12 16 18 30 n0sind 
 |-  ( A e. NN0_s -> ( A = 0s \/ E. x e. NN0_s A = ( x +s 1s ) ) )