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

Metamath Proof Explorer

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	$⊢ (ℕ \times ℕ) \approx ℕ$

Proof

Step	Hyp	Ref	Expression
1		nnenom	$⊢ ℕ \approx ω$
2		xpen	$⊢ (ℕ \approx ω \land ℕ \approx ω) \to (ℕ \times ℕ) \approx (ω \times ω)$
3	1 1 2	mp2an	$⊢ (ℕ \times ℕ) \approx (ω \times ω)$
4		xpomen	$⊢ (ω \times ω) \approx ω$
5	4 1	entr4i	$⊢ (ω \times ω) \approx ℕ$
6	3 5	entri	$⊢ (ℕ \times ℕ) \approx ℕ$