Metamath Proof Explorer

Theorem nnn1suc

Description: A positive integer that is not 1 is a successor of some other positive integer. (Contributed by Steven Nguyen, 19-Aug-2023)

Ref Expression
Assertion nnn1suc 
|- ( ( A e. NN /\ A =/= 1 ) -> E. x e. NN ( x + 1 ) = A )

Proof

Step Hyp Ref Expression
1 neeq1 
 |-  ( y = 1 -> ( y =/= 1 <-> 1 =/= 1 ) )
2 eqeq2 
 |-  ( y = 1 -> ( ( x + 1 ) = y <-> ( x + 1 ) = 1 ) )
3 2 rexbidv 
 |-  ( y = 1 -> ( E. x e. NN ( x + 1 ) = y <-> E. x e. NN ( x + 1 ) = 1 ) )
4 1 3 imbi12d 
 |-  ( y = 1 -> ( ( y =/= 1 -> E. x e. NN ( x + 1 ) = y ) <-> ( 1 =/= 1 -> E. x e. NN ( x + 1 ) = 1 ) ) )
5 neeq1 
 |-  ( y = z -> ( y =/= 1 <-> z =/= 1 ) )
6 eqeq2 
 |-  ( y = z -> ( ( x + 1 ) = y <-> ( x + 1 ) = z ) )
7 6 rexbidv 
 |-  ( y = z -> ( E. x e. NN ( x + 1 ) = y <-> E. x e. NN ( x + 1 ) = z ) )
8 5 7 imbi12d 
 |-  ( y = z -> ( ( y =/= 1 -> E. x e. NN ( x + 1 ) = y ) <-> ( z =/= 1 -> E. x e. NN ( x + 1 ) = z ) ) )
9 neeq1 
 |-  ( y = ( z + 1 ) -> ( y =/= 1 <-> ( z + 1 ) =/= 1 ) )
10 eqeq2 
 |-  ( y = ( z + 1 ) -> ( ( x + 1 ) = y <-> ( x + 1 ) = ( z + 1 ) ) )
11 10 rexbidv 
 |-  ( y = ( z + 1 ) -> ( E. x e. NN ( x + 1 ) = y <-> E. x e. NN ( x + 1 ) = ( z + 1 ) ) )
12 9 11 imbi12d 
 |-  ( y = ( z + 1 ) -> ( ( y =/= 1 -> E. x e. NN ( x + 1 ) = y ) <-> ( ( z + 1 ) =/= 1 -> E. x e. NN ( x + 1 ) = ( z + 1 ) ) ) )
13 neeq1 
 |-  ( y = A -> ( y =/= 1 <-> A =/= 1 ) )
14 eqeq2 
 |-  ( y = A -> ( ( x + 1 ) = y <-> ( x + 1 ) = A ) )
15 14 rexbidv 
 |-  ( y = A -> ( E. x e. NN ( x + 1 ) = y <-> E. x e. NN ( x + 1 ) = A ) )
16 13 15 imbi12d 
 |-  ( y = A -> ( ( y =/= 1 -> E. x e. NN ( x + 1 ) = y ) <-> ( A =/= 1 -> E. x e. NN ( x + 1 ) = A ) ) )
17 df-ne 
 |-  ( 1 =/= 1 <-> -. 1 = 1 )
18 eqid 
 |-  1 = 1
19 18 pm2.24i 
 |-  ( -. 1 = 1 -> E. x e. NN ( x + 1 ) = 1 )
20 17 19 sylbi 
 |-  ( 1 =/= 1 -> E. x e. NN ( x + 1 ) = 1 )
21 id 
 |-  ( z e. NN -> z e. NN )
22 oveq1 
 |-  ( x = z -> ( x + 1 ) = ( z + 1 ) )
23 22 eqeq1d 
 |-  ( x = z -> ( ( x + 1 ) = ( z + 1 ) <-> ( z + 1 ) = ( z + 1 ) ) )
24 23 adantl 
 |-  ( ( z e. NN /\ x = z ) -> ( ( x + 1 ) = ( z + 1 ) <-> ( z + 1 ) = ( z + 1 ) ) )
25 eqidd 
 |-  ( z e. NN -> ( z + 1 ) = ( z + 1 ) )
26 21 24 25 rspcedvd 
 |-  ( z e. NN -> E. x e. NN ( x + 1 ) = ( z + 1 ) )
27 26 2a1d 
 |-  ( z e. NN -> ( ( z =/= 1 -> E. x e. NN ( x + 1 ) = z ) -> ( ( z + 1 ) =/= 1 -> E. x e. NN ( x + 1 ) = ( z + 1 ) ) ) )
28 4 8 12 16 20 27 nnind 
 |-  ( A e. NN -> ( A =/= 1 -> E. x e. NN ( x + 1 ) = A ) )
29 28 imp 
 |-  ( ( A e. NN /\ A =/= 1 ) -> E. x e. NN ( x + 1 ) = A )