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	$$⊢\mathbb{Z}\approx \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
2		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
3	2	ensymi	$$⊢\mathrm{\omega }\approx \mathbb{N}$$
4		isnumi	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{\omega }\approx \mathbb{N}\right)\to \mathbb{N}\in \mathrm{dom}\mathrm{card}$$
5	1 3 4	mp2an	$$⊢\mathbb{N}\in \mathrm{dom}\mathrm{card}$$
6		xpnum	$$⊢\left(\mathbb{N}\in \mathrm{dom}\mathrm{card}\wedge \mathbb{N}\in \mathrm{dom}\mathrm{card}\right)\to \mathbb{N}\times \mathbb{N}\in \mathrm{dom}\mathrm{card}$$
7	5 5 6	mp2an	$$⊢\mathbb{N}\times \mathbb{N}\in \mathrm{dom}\mathrm{card}$$
8		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
9		ffun	$$⊢-:ℂ\times ℂ⟶ℂ\to \mathrm{Fun}-$$
10	8 9	ax-mp	$$⊢\mathrm{Fun}-$$
11		nnsscn	$$⊢\mathbb{N}\subseteq ℂ$$
12		xpss12	$$⊢\left(\mathbb{N}\subseteq ℂ\wedge \mathbb{N}\subseteq ℂ\right)\to \mathbb{N}\times \mathbb{N}\subseteq ℂ\times ℂ$$
13	11 11 12	mp2an	$$⊢\mathbb{N}\times \mathbb{N}\subseteq ℂ\times ℂ$$
14	8	fdmi	$$⊢\mathrm{dom}-=ℂ\times ℂ$$
15	13 14	sseqtrri	$$⊢\mathbb{N}\times \mathbb{N}\subseteq \mathrm{dom}-$$
16		fores	$$⊢\left(\mathrm{Fun}-\wedge \mathbb{N}\times \mathbb{N}\subseteq \mathrm{dom}-\right)\to \left({-\upharpoonright }_{\left(\mathbb{N}\times \mathbb{N}\right)}\right):\mathbb{N}\times \mathbb{N}\underset{onto}{⟶}-\left[\mathbb{N}\times \mathbb{N}\right]$$
17	10 15 16	mp2an	$$⊢\left({-\upharpoonright }_{\left(\mathbb{N}\times \mathbb{N}\right)}\right):\mathbb{N}\times \mathbb{N}\underset{onto}{⟶}-\left[\mathbb{N}\times \mathbb{N}\right]$$
18		dfz2	$$⊢\mathbb{Z}=-\left[\mathbb{N}\times \mathbb{N}\right]$$
19		foeq3	$$⊢\mathbb{Z}=-\left[\mathbb{N}\times \mathbb{N}\right]\to \left(\left({-\upharpoonright }_{\left(\mathbb{N}\times \mathbb{N}\right)}\right):\mathbb{N}\times \mathbb{N}\underset{onto}{⟶}\mathbb{Z}\leftrightarrow \left({-\upharpoonright }_{\left(\mathbb{N}\times \mathbb{N}\right)}\right):\mathbb{N}\times \mathbb{N}\underset{onto}{⟶}-\left[\mathbb{N}\times \mathbb{N}\right]\right)$$
20	18 19	ax-mp	$$⊢\left({-\upharpoonright }_{\left(\mathbb{N}\times \mathbb{N}\right)}\right):\mathbb{N}\times \mathbb{N}\underset{onto}{⟶}\mathbb{Z}\leftrightarrow \left({-\upharpoonright }_{\left(\mathbb{N}\times \mathbb{N}\right)}\right):\mathbb{N}\times \mathbb{N}\underset{onto}{⟶}-\left[\mathbb{N}\times \mathbb{N}\right]$$
21	17 20	mpbir	$$⊢\left({-\upharpoonright }_{\left(\mathbb{N}\times \mathbb{N}\right)}\right):\mathbb{N}\times \mathbb{N}\underset{onto}{⟶}\mathbb{Z}$$
22		fodomnum	$$⊢\mathbb{N}\times \mathbb{N}\in \mathrm{dom}\mathrm{card}\to \left(\left({-\upharpoonright }_{\left(\mathbb{N}\times \mathbb{N}\right)}\right):\mathbb{N}\times \mathbb{N}\underset{onto}{⟶}\mathbb{Z}\to \mathbb{Z}\preccurlyeq \left(\mathbb{N}\times \mathbb{N}\right)\right)$$
23	7 21 22	mp2	$$⊢\mathbb{Z}\preccurlyeq \left(\mathbb{N}\times \mathbb{N}\right)$$
24		xpnnen	$$⊢\left(\mathbb{N}\times \mathbb{N}\right)\approx \mathbb{N}$$
25		domentr	$$⊢\left(\mathbb{Z}\preccurlyeq \left(\mathbb{N}\times \mathbb{N}\right)\wedge \left(\mathbb{N}\times \mathbb{N}\right)\approx \mathbb{N}\right)\to \mathbb{Z}\preccurlyeq \mathbb{N}$$
26	23 24 25	mp2an	$$⊢\mathbb{Z}\preccurlyeq \mathbb{N}$$
27		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
28		nnssz	$$⊢\mathbb{N}\subseteq \mathbb{Z}$$
29		ssdomg	$$⊢\mathbb{Z}\in \mathrm{V}\to \left(\mathbb{N}\subseteq \mathbb{Z}\to \mathbb{N}\preccurlyeq \mathbb{Z}\right)$$
30	27 28 29	mp2	$$⊢\mathbb{N}\preccurlyeq \mathbb{Z}$$
31		sbth	$$⊢\left(\mathbb{Z}\preccurlyeq \mathbb{N}\wedge \mathbb{N}\preccurlyeq \mathbb{Z}\right)\to \mathbb{Z}\approx \mathbb{N}$$
32	26 30 31	mp2an	$$⊢\mathbb{Z}\approx \mathbb{N}$$