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

Metamath Proof Explorer

Theorem nnf1oxpnn

Description: There is a bijection between the set of positive integers and the Cartesian product of the set of positive integers with itself. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Assertion	nnf1oxpnn	$⊢ \exists f f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$

Proof

Step	Hyp	Ref	Expression
1		xpnnen	$⊢ (ℕ \times ℕ) \approx ℕ$
2	1	ensymi	$⊢ ℕ \approx (ℕ \times ℕ)$
3		bren	$⊢ ℕ \approx (ℕ \times ℕ) \leftrightarrow \exists f f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
4	2 3	mpbi	$⊢ \exists f f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$