Metamath Proof Explorer

Theorem nn0ennn

Description: The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004)

Ref Expression
Assertion nn0ennn 
|- NN0 ~~ NN

Proof

Step Hyp Ref Expression
1 nn0ex 
 |-  NN0 e. _V
2 nnex 
 |-  NN e. _V
3 nn0p1nn 
 |-  ( x e. NN0 -> ( x + 1 ) e. NN )
4 nnm1nn0 
 |-  ( y e. NN -> ( y - 1 ) e. NN0 )
5 nncn 
 |-  ( y e. NN -> y e. CC )
6 nn0cn 
 |-  ( x e. NN0 -> x e. CC )
7 ax-1cn 
 |-  1 e. CC
8 subadd 
 |-  ( ( y e. CC /\ 1 e. CC /\ x e. CC ) -> ( ( y - 1 ) = x <-> ( 1 + x ) = y ) )
9 7 8 mp3an2 
 |-  ( ( y e. CC /\ x e. CC ) -> ( ( y - 1 ) = x <-> ( 1 + x ) = y ) )
10 eqcom 
 |-  ( x = ( y - 1 ) <-> ( y - 1 ) = x )
11 eqcom 
 |-  ( y = ( 1 + x ) <-> ( 1 + x ) = y )
12 9 10 11 3bitr4g 
 |-  ( ( y e. CC /\ x e. CC ) -> ( x = ( y - 1 ) <-> y = ( 1 + x ) ) )
13 addcom 
 |-  ( ( 1 e. CC /\ x e. CC ) -> ( 1 + x ) = ( x + 1 ) )
14 7 13 mpan 
 |-  ( x e. CC -> ( 1 + x ) = ( x + 1 ) )
15 14 eqeq2d 
 |-  ( x e. CC -> ( y = ( 1 + x ) <-> y = ( x + 1 ) ) )
16 15 adantl 
 |-  ( ( y e. CC /\ x e. CC ) -> ( y = ( 1 + x ) <-> y = ( x + 1 ) ) )
17 12 16 bitrd 
 |-  ( ( y e. CC /\ x e. CC ) -> ( x = ( y - 1 ) <-> y = ( x + 1 ) ) )
18 5 6 17 syl2anr 
 |-  ( ( x e. NN0 /\ y e. NN ) -> ( x = ( y - 1 ) <-> y = ( x + 1 ) ) )
19 1 2 3 4 18 en3i 
 |-  NN0 ~~ NN