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 { 1 , 2 } to the real numbers). (Contributed by AV, 12-Mar-2023)

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

Proof

Step	Hyp	Ref	Expression
1		rrx2xpreen.r	$⊢ R = ℝ^{\{1, 2\}}$
2		rrx2xpref1o.1	$⊢ F = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\})$
3		prex	$⊢ \{⟨1, x⟩, ⟨2, y⟩\} \in V$
4	2 3	fnmpoi	$⊢ F Fn ℝ^{2}$
5		1st2nd2	$⊢ z \in ℝ^{2} \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
6	5	fveq2d	$⊢ z \in ℝ^{2} \to F (z) = F (⟨1^{st} (z), 2^{nd} (z)⟩)$
7		df-ov	$⊢ 1^{st} (z) F 2^{nd} (z) = F (⟨1^{st} (z), 2^{nd} (z)⟩)$
8	6 7	eqtr4di	$⊢ z \in ℝ^{2} \to F (z) = 1^{st} (z) F 2^{nd} (z)$
9		xp1st	$⊢ z \in ℝ^{2} \to 1^{st} (z) \in ℝ$
10		xp2nd	$⊢ z \in ℝ^{2} \to 2^{nd} (z) \in ℝ$
11		opeq2	$⊢ x = 1^{st} (z) \to ⟨1, x⟩ = ⟨1, 1^{st} (z)⟩$
12	11	preq1d	$⊢ x = 1^{st} (z) \to \{⟨1, x⟩, ⟨2, y⟩\} = \{⟨1, 1^{st} (z)⟩, ⟨2, y⟩\}$
13		opeq2	$⊢ y = 2^{nd} (z) \to ⟨2, y⟩ = ⟨2, 2^{nd} (z)⟩$
14	13	preq2d	$⊢ y = 2^{nd} (z) \to \{⟨1, 1^{st} (z)⟩, ⟨2, y⟩\} = \{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\}$
15		prex	$⊢ \{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\} \in V$
16	12 14 2 15	ovmpo	$⊢ (1^{st} (z) \in ℝ \land 2^{nd} (z) \in ℝ) \to 1^{st} (z) F 2^{nd} (z) = \{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\}$
17	9 10 16	syl2anc	$⊢ z \in ℝ^{2} \to 1^{st} (z) F 2^{nd} (z) = \{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\}$
18	8 17	eqtrd	$⊢ z \in ℝ^{2} \to F (z) = \{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\}$
19		eqid	$⊢ \{1, 2\} = \{1, 2\}$
20	19 1	prelrrx2	$⊢ (1^{st} (z) \in ℝ \land 2^{nd} (z) \in ℝ) \to \{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\} \in R$
21	9 10 20	syl2anc	$⊢ z \in ℝ^{2} \to \{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\} \in R$
22	18 21	eqeltrd	$⊢ z \in ℝ^{2} \to F (z) \in R$
23	22	rgen	$⊢ \forall z \in ℝ^{2} F (z) \in R$
24		ffnfv	$⊢ F : ℝ^{2} ⟶ R \leftrightarrow (F Fn ℝ^{2} \land \forall z \in ℝ^{2} F (z) \in R)$
25	4 23 24	mpbir2an	$⊢ F : ℝ^{2} ⟶ R$
26		opex	$⊢ ⟨1, 1^{st} (z)⟩ \in V$
27		opex	$⊢ ⟨2, 2^{nd} (z)⟩ \in V$
28		opex	$⊢ ⟨1, 1^{st} (w)⟩ \in V$
29		opex	$⊢ ⟨2, 2^{nd} (w)⟩ \in V$
30	26 27 28 29	preq12b	$⊢ \{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\} = \{⟨1, 1^{st} (w)⟩, ⟨2, 2^{nd} (w)⟩\} \leftrightarrow ((⟨1, 1^{st} (z)⟩ = ⟨1, 1^{st} (w)⟩ \land ⟨2, 2^{nd} (z)⟩ = ⟨2, 2^{nd} (w)⟩) \lor (⟨1, 1^{st} (z)⟩ = ⟨2, 2^{nd} (w)⟩ \land ⟨2, 2^{nd} (z)⟩ = ⟨1, 1^{st} (w)⟩))$
31		1ex	$⊢ 1 \in V$
32		fvex	$⊢ 1^{st} (z) \in V$
33	31 32	opth	$⊢ ⟨1, 1^{st} (z)⟩ = ⟨1, 1^{st} (w)⟩ \leftrightarrow (1 = 1 \land 1^{st} (z) = 1^{st} (w))$
34	33	simprbi	$⊢ ⟨1, 1^{st} (z)⟩ = ⟨1, 1^{st} (w)⟩ \to 1^{st} (z) = 1^{st} (w)$
35		2ex	$⊢ 2 \in V$
36		fvex	$⊢ 2^{nd} (z) \in V$
37	35 36	opth	$⊢ ⟨2, 2^{nd} (z)⟩ = ⟨2, 2^{nd} (w)⟩ \leftrightarrow (2 = 2 \land 2^{nd} (z) = 2^{nd} (w))$
38	37	simprbi	$⊢ ⟨2, 2^{nd} (z)⟩ = ⟨2, 2^{nd} (w)⟩ \to 2^{nd} (z) = 2^{nd} (w)$
39	34 38	anim12i	$⊢ (⟨1, 1^{st} (z)⟩ = ⟨1, 1^{st} (w)⟩ \land ⟨2, 2^{nd} (z)⟩ = ⟨2, 2^{nd} (w)⟩) \to (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w))$
40	39	a1d	$⊢ (⟨1, 1^{st} (z)⟩ = ⟨1, 1^{st} (w)⟩ \land ⟨2, 2^{nd} (z)⟩ = ⟨2, 2^{nd} (w)⟩) \to ((z \in ℝ^{2} \land w \in ℝ^{2}) \to (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w)))$
41	31 32	opth	$⊢ ⟨1, 1^{st} (z)⟩ = ⟨2, 2^{nd} (w)⟩ \leftrightarrow (1 = 2 \land 1^{st} (z) = 2^{nd} (w))$
42	35 36	opth	$⊢ ⟨2, 2^{nd} (z)⟩ = ⟨1, 1^{st} (w)⟩ \leftrightarrow (2 = 1 \land 2^{nd} (z) = 1^{st} (w))$
43		1ne2	$⊢ 1 \neq 2$
44		eqneqall	$⊢ 1 = 2 \to (1 \neq 2 \to ((z \in ℝ^{2} \land w \in ℝ^{2}) \to (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w))))$
45	43 44	mpi	$⊢ 1 = 2 \to ((z \in ℝ^{2} \land w \in ℝ^{2}) \to (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w)))$
46	45	ad2antrr	$⊢ ((1 = 2 \land 1^{st} (z) = 2^{nd} (w)) \land (2 = 1 \land 2^{nd} (z) = 1^{st} (w))) \to ((z \in ℝ^{2} \land w \in ℝ^{2}) \to (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w)))$
47	41 42 46	syl2anb	$⊢ (⟨1, 1^{st} (z)⟩ = ⟨2, 2^{nd} (w)⟩ \land ⟨2, 2^{nd} (z)⟩ = ⟨1, 1^{st} (w)⟩) \to ((z \in ℝ^{2} \land w \in ℝ^{2}) \to (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w)))$
48	40 47	jaoi	$⊢ ((⟨1, 1^{st} (z)⟩ = ⟨1, 1^{st} (w)⟩ \land ⟨2, 2^{nd} (z)⟩ = ⟨2, 2^{nd} (w)⟩) \lor (⟨1, 1^{st} (z)⟩ = ⟨2, 2^{nd} (w)⟩ \land ⟨2, 2^{nd} (z)⟩ = ⟨1, 1^{st} (w)⟩)) \to ((z \in ℝ^{2} \land w \in ℝ^{2}) \to (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w)))$
49	30 48	sylbi	$⊢ \{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\} = \{⟨1, 1^{st} (w)⟩, ⟨2, 2^{nd} (w)⟩\} \to ((z \in ℝ^{2} \land w \in ℝ^{2}) \to (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w)))$
50	49	com12	$⊢ (z \in ℝ^{2} \land w \in ℝ^{2}) \to (\{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\} = \{⟨1, 1^{st} (w)⟩, ⟨2, 2^{nd} (w)⟩\} \to (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w)))$
51		1st2nd2	$⊢ w \in ℝ^{2} \to w = ⟨1^{st} (w), 2^{nd} (w)⟩$
52	51	fveq2d	$⊢ w \in ℝ^{2} \to F (w) = F (⟨1^{st} (w), 2^{nd} (w)⟩)$
53		df-ov	$⊢ 1^{st} (w) F 2^{nd} (w) = F (⟨1^{st} (w), 2^{nd} (w)⟩)$
54	52 53	eqtr4di	$⊢ w \in ℝ^{2} \to F (w) = 1^{st} (w) F 2^{nd} (w)$
55		xp1st	$⊢ w \in ℝ^{2} \to 1^{st} (w) \in ℝ$
56		xp2nd	$⊢ w \in ℝ^{2} \to 2^{nd} (w) \in ℝ$
57		opeq2	$⊢ x = 1^{st} (w) \to ⟨1, x⟩ = ⟨1, 1^{st} (w)⟩$
58	57	preq1d	$⊢ x = 1^{st} (w) \to \{⟨1, x⟩, ⟨2, y⟩\} = \{⟨1, 1^{st} (w)⟩, ⟨2, y⟩\}$
59		opeq2	$⊢ y = 2^{nd} (w) \to ⟨2, y⟩ = ⟨2, 2^{nd} (w)⟩$
60	59	preq2d	$⊢ y = 2^{nd} (w) \to \{⟨1, 1^{st} (w)⟩, ⟨2, y⟩\} = \{⟨1, 1^{st} (w)⟩, ⟨2, 2^{nd} (w)⟩\}$
61		prex	$⊢ \{⟨1, 1^{st} (w)⟩, ⟨2, 2^{nd} (w)⟩\} \in V$
62	58 60 2 61	ovmpo	$⊢ (1^{st} (w) \in ℝ \land 2^{nd} (w) \in ℝ) \to 1^{st} (w) F 2^{nd} (w) = \{⟨1, 1^{st} (w)⟩, ⟨2, 2^{nd} (w)⟩\}$
63	55 56 62	syl2anc	$⊢ w \in ℝ^{2} \to 1^{st} (w) F 2^{nd} (w) = \{⟨1, 1^{st} (w)⟩, ⟨2, 2^{nd} (w)⟩\}$
64	54 63	eqtrd	$⊢ w \in ℝ^{2} \to F (w) = \{⟨1, 1^{st} (w)⟩, ⟨2, 2^{nd} (w)⟩\}$
65	18 64	eqeqan12d	$⊢ (z \in ℝ^{2} \land w \in ℝ^{2}) \to (F (z) = F (w) \leftrightarrow \{⟨1, 1^{st} (z)⟩, ⟨2, 2^{nd} (z)⟩\} = \{⟨1, 1^{st} (w)⟩, ⟨2, 2^{nd} (w)⟩\})$
66	5 51	eqeqan12d	$⊢ (z \in ℝ^{2} \land w \in ℝ^{2}) \to (z = w \leftrightarrow ⟨1^{st} (z), 2^{nd} (z)⟩ = ⟨1^{st} (w), 2^{nd} (w)⟩)$
67	32 36	opth	$⊢ ⟨1^{st} (z), 2^{nd} (z)⟩ = ⟨1^{st} (w), 2^{nd} (w)⟩ \leftrightarrow (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w))$
68	66 67	bitrdi	$⊢ (z \in ℝ^{2} \land w \in ℝ^{2}) \to (z = w \leftrightarrow (1^{st} (z) = 1^{st} (w) \land 2^{nd} (z) = 2^{nd} (w)))$
69	50 65 68	3imtr4d	$⊢ (z \in ℝ^{2} \land w \in ℝ^{2}) \to (F (z) = F (w) \to z = w)$
70	69	rgen2	$⊢ \forall z \in ℝ^{2} \forall w \in ℝ^{2} (F (z) = F (w) \to z = w)$
71		dff13	$⊢ F : ℝ^{2} \underset{1-1}{⟶} R \leftrightarrow (F : ℝ^{2} ⟶ R \land \forall z \in ℝ^{2} \forall w \in ℝ^{2} (F (z) = F (w) \to z = w))$
72	25 70 71	mpbir2an	$⊢ F : ℝ^{2} \underset{1-1}{⟶} R$
73	1	eleq2i	$⊢ w \in R \leftrightarrow w \in (ℝ^{\{1, 2\}})$
74		reex	$⊢ ℝ \in V$
75		prex	$⊢ \{1, 2\} \in V$
76	74 75	elmap	$⊢ w \in (ℝ^{\{1, 2\}}) \leftrightarrow w : \{1, 2\} ⟶ ℝ$
77		1re	$⊢ 1 \in ℝ$
78		2re	$⊢ 2 \in ℝ$
79		fpr2g	$⊢ (1 \in ℝ \land 2 \in ℝ) \to (w : \{1, 2\} ⟶ ℝ \leftrightarrow (w (1) \in ℝ \land w (2) \in ℝ \land w = \{⟨1, w (1)⟩, ⟨2, w (2)⟩\}))$
80	77 78 79	mp2an	$⊢ w : \{1, 2\} ⟶ ℝ \leftrightarrow (w (1) \in ℝ \land w (2) \in ℝ \land w = \{⟨1, w (1)⟩, ⟨2, w (2)⟩\})$
81	73 76 80	3bitri	$⊢ w \in R \leftrightarrow (w (1) \in ℝ \land w (2) \in ℝ \land w = \{⟨1, w (1)⟩, ⟨2, w (2)⟩\})$
82		opeq2	$⊢ u = w (1) \to ⟨1, u⟩ = ⟨1, w (1)⟩$
83	82	preq1d	$⊢ u = w (1) \to \{⟨1, u⟩, ⟨2, v⟩\} = \{⟨1, w (1)⟩, ⟨2, v⟩\}$
84	83	eqeq2d	$⊢ u = w (1) \to (w = \{⟨1, u⟩, ⟨2, v⟩\} \leftrightarrow w = \{⟨1, w (1)⟩, ⟨2, v⟩\})$
85		opeq2	$⊢ v = w (2) \to ⟨2, v⟩ = ⟨2, w (2)⟩$
86	85	preq2d	$⊢ v = w (2) \to \{⟨1, w (1)⟩, ⟨2, v⟩\} = \{⟨1, w (1)⟩, ⟨2, w (2)⟩\}$
87	86	eqeq2d	$⊢ v = w (2) \to (w = \{⟨1, w (1)⟩, ⟨2, v⟩\} \leftrightarrow w = \{⟨1, w (1)⟩, ⟨2, w (2)⟩\})$
88	84 87	rspc2ev	$⊢ (w (1) \in ℝ \land w (2) \in ℝ \land w = \{⟨1, w (1)⟩, ⟨2, w (2)⟩\}) \to \exists u \in ℝ \exists v \in ℝ w = \{⟨1, u⟩, ⟨2, v⟩\}$
89	81 88	sylbi	$⊢ w \in R \to \exists u \in ℝ \exists v \in ℝ w = \{⟨1, u⟩, ⟨2, v⟩\}$
90		opeq2	$⊢ x = u \to ⟨1, x⟩ = ⟨1, u⟩$
91	90	preq1d	$⊢ x = u \to \{⟨1, x⟩, ⟨2, y⟩\} = \{⟨1, u⟩, ⟨2, y⟩\}$
92		opeq2	$⊢ y = v \to ⟨2, y⟩ = ⟨2, v⟩$
93	92	preq2d	$⊢ y = v \to \{⟨1, u⟩, ⟨2, y⟩\} = \{⟨1, u⟩, ⟨2, v⟩\}$
94		prex	$⊢ \{⟨1, u⟩, ⟨2, v⟩\} \in V$
95	91 93 2 94	ovmpo	$⊢ (u \in ℝ \land v \in ℝ) \to u F v = \{⟨1, u⟩, ⟨2, v⟩\}$
96	95	eqeq2d	$⊢ (u \in ℝ \land v \in ℝ) \to (w = u F v \leftrightarrow w = \{⟨1, u⟩, ⟨2, v⟩\})$
97	96	2rexbiia	$⊢ \exists u \in ℝ \exists v \in ℝ w = u F v \leftrightarrow \exists u \in ℝ \exists v \in ℝ w = \{⟨1, u⟩, ⟨2, v⟩\}$
98	89 97	sylibr	$⊢ w \in R \to \exists u \in ℝ \exists v \in ℝ w = u F v$
99		fveq2	$⊢ z = ⟨u, v⟩ \to F (z) = F (⟨u, v⟩)$
100		df-ov	$⊢ u F v = F (⟨u, v⟩)$
101	99 100	eqtr4di	$⊢ z = ⟨u, v⟩ \to F (z) = u F v$
102	101	eqeq2d	$⊢ z = ⟨u, v⟩ \to (w = F (z) \leftrightarrow w = u F v)$
103	102	rexxp	$⊢ \exists z \in ℝ^{2} w = F (z) \leftrightarrow \exists u \in ℝ \exists v \in ℝ w = u F v$
104	98 103	sylibr	$⊢ w \in R \to \exists z \in ℝ^{2} w = F (z)$
105	104	rgen	$⊢ \forall w \in R \exists z \in ℝ^{2} w = F (z)$
106		dffo3	$⊢ F : ℝ^{2} \underset{onto}{⟶} R \leftrightarrow (F : ℝ^{2} ⟶ R \land \forall w \in R \exists z \in ℝ^{2} w = F (z))$
107	25 105 106	mpbir2an	$⊢ F : ℝ^{2} \underset{onto}{⟶} R$
108		df-f1o	$⊢ F : ℝ^{2} \underset{1-1 onto}{⟶} R \leftrightarrow (F : ℝ^{2} \underset{1-1}{⟶} R \land F : ℝ^{2} \underset{onto}{⟶} R)$
109	72 107 108	mpbir2an	$⊢ F : ℝ^{2} \underset{1-1 onto}{⟶} R$

Metamath Proof Explorer

Theorem rrx2xpref1o

Proof