Theorem xpnnen

Description: The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004) (Revised by Mario Carneiro, 9-Mar-2013)

	Ref	Expression
Assertion	xpnnen	$$⊢\left(\mathbb{N}\times \mathbb{N}\right)\approx \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
2		xpen	$$⊢\left(\mathbb{N}\approx \mathrm{\omega }\wedge \mathbb{N}\approx \mathrm{\omega }\right)\to \left(\mathbb{N}\times \mathbb{N}\right)\approx \left(\mathrm{\omega }\times \mathrm{\omega }\right)$$
3	1 1 2	mp2an	$$⊢\left(\mathbb{N}\times \mathbb{N}\right)\approx \left(\mathrm{\omega }\times \mathrm{\omega }\right)$$
4		xpomen	$$⊢\left(\mathrm{\omega }\times \mathrm{\omega }\right)\approx \mathrm{\omega }$$
5	4 1	entr4i	$$⊢\left(\mathrm{\omega }\times \mathrm{\omega }\right)\approx \mathbb{N}$$
6	3 5	entri	$$⊢\left(\mathbb{N}\times \mathbb{N}\right)\approx \mathbb{N}$$