rrx2xpref1o

Description: There is a bijection between the set of ordered pairs of real numbers (the cartesian product of the real numbers) and the set of points in the two dimensional Euclidean plane (represented as mappings from ( 0 ..^ 2 ) to the real numbers). (Contributed by AV, 12-Mar-2023)

	Ref	Expression
Hypotheses	rrx2xpreen.r	$⊢ R = ℝ^{(0 ..^2)}$
	rrx2xpref1o.1	$⊢ F = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩)$
Assertion	rrx2xpref1o	$⊢ F : ℝ^{2} \underset{1-1 onto}{⟶} R$

Proof

Step	Hyp	Ref	Expression
1		rrx2xpreen.r	$⊢ R = ℝ^{(0 ..^2)}$
2		rrx2xpref1o.1	$⊢ F = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩)$
3		simprl	$⊢ (⊤ \land (x \in ℝ \land y \in ℝ)) \to x \in ℝ$
4		simprr	$⊢ (⊤ \land (x \in ℝ \land y \in ℝ)) \to y \in ℝ$
5	3 4	s2cld	$⊢ (⊤ \land (x \in ℝ \land y \in ℝ)) \to ⟨“ x y ”⟩ \in Word ℝ$
6		eqid	$⊢ (0 ..^2) = (0 ..^2)$
7	6 1	rrx2pxel	$⊢ z \in R \to z (0) \in ℝ$
8	6 1	rrx2pyel	$⊢ z \in R \to z (1) \in ℝ$
9	7 8	jca	$⊢ z \in R \to (z (0) \in ℝ \land z (1) \in ℝ)$
10	9	adantl	$⊢ (⊤ \land z \in R) \to (z (0) \in ℝ \land z (1) \in ℝ)$
11		simprl	$⊢ (z \in R \land (z (0) = x \land z (1) = y)) \to z (0) = x$
12	7	adantr	$⊢ (z \in R \land (z (0) = x \land z (1) = y)) \to z (0) \in ℝ$
13	11 12	eqeltrrd	$⊢ (z \in R \land (z (0) = x \land z (1) = y)) \to x \in ℝ$
14		simprr	$⊢ (z \in R \land (z (0) = x \land z (1) = y)) \to z (1) = y$
15	8	adantr	$⊢ (z \in R \land (z (0) = x \land z (1) = y)) \to z (1) \in ℝ$
16	14 15	eqeltrrd	$⊢ (z \in R \land (z (0) = x \land z (1) = y)) \to y \in ℝ$
17	13 16	jca	$⊢ (z \in R \land (z (0) = x \land z (1) = y)) \to (x \in ℝ \land y \in ℝ)$
18	17	pm4.71ri	$⊢ (z \in R \land (z (0) = x \land z (1) = y)) \leftrightarrow ((x \in ℝ \land y \in ℝ) \land (z \in R \land (z (0) = x \land z (1) = y)))$
19		eqcom	$⊢ x = z (0) \leftrightarrow z (0) = x$
20		eqcom	$⊢ y = z (1) \leftrightarrow z (1) = y$
21	19 20	anbi12i	$⊢ (x = z (0) \land y = z (1)) \leftrightarrow (z (0) = x \land z (1) = y)$
22	21	anbi2i	$⊢ (z \in R \land (x = z (0) \land y = z (1))) \leftrightarrow (z \in R \land (z (0) = x \land z (1) = y))$
23		simpl	$⊢ (x \in ℝ \land y \in ℝ) \to x \in ℝ$
24		simpr	$⊢ (x \in ℝ \land y \in ℝ) \to y \in ℝ$
25	6 1 23 24	prelrrx2bd	$⊢ (x \in ℝ \land y \in ℝ) \to (z = ⟨“ x y ”⟩ \leftrightarrow (z \in R \land (z (0) = x \land z (1) = y)))$
26	25	pm5.32i	$⊢ ((x \in ℝ \land y \in ℝ) \land z = ⟨“ x y ”⟩) \leftrightarrow ((x \in ℝ \land y \in ℝ) \land (z \in R \land (z (0) = x \land z (1) = y)))$
27	18 22 26	3bitr4ri	$⊢ ((x \in ℝ \land y \in ℝ) \land z = ⟨“ x y ”⟩) \leftrightarrow (z \in R \land (x = z (0) \land y = z (1)))$
28	27	a1i	$⊢ ⊤ \to (((x \in ℝ \land y \in ℝ) \land z = ⟨“ x y ”⟩) \leftrightarrow (z \in R \land (x = z (0) \land y = z (1))))$
29	2 5 10 28	f1od2	$⊢ ⊤ \to F : ℝ^{2} \underset{1-1 onto}{⟶} R$
30	29	mptru	$⊢ F : ℝ^{2} \underset{1-1 onto}{⟶} R$

Metamath Proof Explorer

Theorem rrx2xpref1o

Proof