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	⊢ ( ℕ × ℕ ) ≈ ℕ

Proof

Step	Hyp	Ref	Expression
1		nnenom	⊢ ℕ ≈ ω
2		xpen	⊢ ( ( ℕ ≈ ω ∧ ℕ ≈ ω ) → ( ℕ × ℕ ) ≈ ( ω × ω ) )
3	1 1 2	mp2an	⊢ ( ℕ × ℕ ) ≈ ( ω × ω )
4		xpomen	⊢ ( ω × ω ) ≈ ω
5	4 1	entr4i	⊢ ( ω × ω ) ≈ ℕ
6	3 5	entri	⊢ ( ℕ × ℕ ) ≈ ℕ