This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem znnen

Description: The set of integers and the set of positive integers are equinumerous. Exercise 1 of Gleason p. 140. (Contributed by NM, 31-Jul-2004) (Proof shortened by Mario Carneiro, 13-Jun-2014)

Ref Expression
Assertion znnen 
|- ZZ ~~ NN

Proof

Step Hyp Ref Expression
1 omelon 
 |-  _om e. On
2 nnenom 
 |-  NN ~~ _om
3 2 ensymi 
 |-  _om ~~ NN
4 isnumi 
 |-  ( ( _om e. On /\ _om ~~ NN ) -> NN e. dom card )
5 1 3 4 mp2an 
 |-  NN e. dom card
6 xpnum 
 |-  ( ( NN e. dom card /\ NN e. dom card ) -> ( NN X. NN ) e. dom card )
7 5 5 6 mp2an 
 |-  ( NN X. NN ) e. dom card
8 subf 
 |-  - : ( CC X. CC ) --> CC
9 ffun 
 |-  ( - : ( CC X. CC ) --> CC -> Fun - )
10 8 9 ax-mp 
 |-  Fun -
11 nnsscn 
 |-  NN C_ CC
12 xpss12 
 |-  ( ( NN C_ CC /\ NN C_ CC ) -> ( NN X. NN ) C_ ( CC X. CC ) )
13 11 11 12 mp2an 
 |-  ( NN X. NN ) C_ ( CC X. CC )
14 8 fdmi 
 |-  dom - = ( CC X. CC )
15 13 14 sseqtrri 
 |-  ( NN X. NN ) C_ dom -
16 fores 
 |-  ( ( Fun - /\ ( NN X. NN ) C_ dom - ) -> ( - |` ( NN X. NN ) ) : ( NN X. NN ) -onto-> ( - " ( NN X. NN ) ) )
17 10 15 16 mp2an 
 |-  ( - |` ( NN X. NN ) ) : ( NN X. NN ) -onto-> ( - " ( NN X. NN ) )
18 dfz2 
 |-  ZZ = ( - " ( NN X. NN ) )
19 foeq3 
 |-  ( ZZ = ( - " ( NN X. NN ) ) -> ( ( - |` ( NN X. NN ) ) : ( NN X. NN ) -onto-> ZZ <-> ( - |` ( NN X. NN ) ) : ( NN X. NN ) -onto-> ( - " ( NN X. NN ) ) ) )
20 18 19 ax-mp 
 |-  ( ( - |` ( NN X. NN ) ) : ( NN X. NN ) -onto-> ZZ <-> ( - |` ( NN X. NN ) ) : ( NN X. NN ) -onto-> ( - " ( NN X. NN ) ) )
21 17 20 mpbir 
 |-  ( - |` ( NN X. NN ) ) : ( NN X. NN ) -onto-> ZZ
22 fodomnum 
 |-  ( ( NN X. NN ) e. dom card -> ( ( - |` ( NN X. NN ) ) : ( NN X. NN ) -onto-> ZZ -> ZZ ~<_ ( NN X. NN ) ) )
23 7 21 22 mp2 
 |-  ZZ ~<_ ( NN X. NN )
24 xpnnen 
 |-  ( NN X. NN ) ~~ NN
25 domentr 
 |-  ( ( ZZ ~<_ ( NN X. NN ) /\ ( NN X. NN ) ~~ NN ) -> ZZ ~<_ NN )
26 23 24 25 mp2an 
 |-  ZZ ~<_ NN
27 zex 
 |-  ZZ e. _V
28 nnssz 
 |-  NN C_ ZZ
29 ssdomg 
 |-  ( ZZ e. _V -> ( NN C_ ZZ -> NN ~<_ ZZ ) )
30 27 28 29 mp2 
 |-  NN ~<_ ZZ
31 sbth 
 |-  ( ( ZZ ~<_ NN /\ NN ~<_ ZZ ) -> ZZ ~~ NN )
32 26 30 31 mp2an 
 |-  ZZ ~~ NN