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 ff:\mathbb{N}\underset{1-1\; onto}{⟶}\mathbb{N}\times \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		xpnnen	$$⊢\left(\mathbb{N}\times \mathbb{N}\right)\approx \mathbb{N}$$
2	1	ensymi	$$⊢\mathbb{N}\approx \left(\mathbb{N}\times \mathbb{N}\right)$$
3		bren	$$⊢\mathbb{N}\approx \left(\mathbb{N}\times \mathbb{N}\right)\leftrightarrow \exists ff:\mathbb{N}\underset{1-1\; onto}{⟶}\mathbb{N}\times \mathbb{N}$$
4	2 3	mpbi	$$⊢\exists ff:\mathbb{N}\underset{1-1\; onto}{⟶}\mathbb{N}\times \mathbb{N}$$