Metamath Proof Explorer

Theorem dfz2

Description: Alternative definition of the integers, based on elz2 . (Contributed by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion dfz2 
|- ZZ = ( - " ( NN X. NN ) )

Proof

Step Hyp Ref Expression
1 elz2 
 |-  ( x e. ZZ <-> E. y e. NN E. z e. NN x = ( y - z ) )
2 subf 
 |-  - : ( CC X. CC ) --> CC
3 ffn 
 |-  ( - : ( CC X. CC ) --> CC -> - Fn ( CC X. CC ) )
4 2 3 ax-mp 
 |-  - Fn ( CC X. CC )
5 nnsscn 
 |-  NN C_ CC
6 xpss12 
 |-  ( ( NN C_ CC /\ NN C_ CC ) -> ( NN X. NN ) C_ ( CC X. CC ) )
7 5 5 6 mp2an 
 |-  ( NN X. NN ) C_ ( CC X. CC )
8 ovelimab 
 |-  ( ( - Fn ( CC X. CC ) /\ ( NN X. NN ) C_ ( CC X. CC ) ) -> ( x e. ( - " ( NN X. NN ) ) <-> E. y e. NN E. z e. NN x = ( y - z ) ) )
9 4 7 8 mp2an 
 |-  ( x e. ( - " ( NN X. NN ) ) <-> E. y e. NN E. z e. NN x = ( y - z ) )
10 1 9 bitr4i 
 |-  ( x e. ZZ <-> x e. ( - " ( NN X. NN ) ) )
11 10 eqriv 
 |-  ZZ = ( - " ( NN X. NN ) )