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