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	⊢ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ )

Proof

Step	Hyp	Ref	Expression
1		xpnnen	⊢ ( ℕ × ℕ ) ≈ ℕ
2	1	ensymi	⊢ ℕ ≈ ( ℕ × ℕ )
3		bren	⊢ ( ℕ ≈ ( ℕ × ℕ ) ↔ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) )
4	2 3	mpbi	⊢ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ )