rrx2xpref1o - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > rrx2xpref1o		Structured version Visualization version GIF version

Theorem rrx2xpref1o 49209

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.)

**Hypotheses**
Ref	Expression
rrx2xpreen.r	⊢ 𝑅 = (ℝ ↑_m {1, 2})
rrx2xpref1o.1	⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {⟨1, 𝑥⟩, ⟨2, 𝑦⟩})

**Assertion**
Ref	Expression
rrx2xpref1o	⊢ 𝐹:(ℝ × ℝ)–1-1-onto→𝑅

Distinct variable group: 𝑥,𝑦 Allowed substitution hints: 𝑅(𝑥,𝑦) 𝐹(𝑥,𝑦)

Proof of Theorem rrx2xpref1o Dummy variables 𝑣 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rrx2xpref1o.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {⟨1, 𝑥⟩, ⟨2, 𝑦⟩})
2		prex 5367	. . . . 5 ⊢ {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} ∈ V
3	1, 2	fnmpoi 8012	. . . 4 ⊢ 𝐹 Fn (ℝ × ℝ)
4		1st2nd2 7970	. . . . . . . . 9 ⊢ (𝑧 ∈ (ℝ × ℝ) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
5	4	fveq2d 6831	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = (𝐹‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
6		df-ov 7359	. . . . . . . 8 ⊢ ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)) = (𝐹‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
7	5, 6	eqtr4di 2792	. . . . . . 7 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)))
8		xp1st 7963	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (1^st ‘𝑧) ∈ ℝ)
9		xp2nd 7964	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (2^nd ‘𝑧) ∈ ℝ)
10		opeq2 4805	. . . . . . . . . 10 ⊢ (𝑥 = (1^st ‘𝑧) → ⟨1, 𝑥⟩ = ⟨1, (1^st ‘𝑧)⟩)
11	10	preq1d 4671	. . . . . . . . 9 ⊢ (𝑥 = (1^st ‘𝑧) → {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑧)⟩, ⟨2, 𝑦⟩})
12		opeq2 4805	. . . . . . . . . 10 ⊢ (𝑦 = (2^nd ‘𝑧) → ⟨2, 𝑦⟩ = ⟨2, (2^nd ‘𝑧)⟩)
13	12	preq2d 4672	. . . . . . . . 9 ⊢ (𝑦 = (2^nd ‘𝑧) → {⟨1, (1^st ‘𝑧)⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
14		prex 5367	. . . . . . . . 9 ⊢ {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} ∈ V
15	11, 13, 1, 14	ovmpo 7516	. . . . . . . 8 ⊢ (((1^st ‘𝑧) ∈ ℝ ∧ (2^nd ‘𝑧) ∈ ℝ) → ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)) = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
16	8, 9, 15	syl2anc 590	. . . . . . 7 ⊢ (𝑧 ∈ (ℝ × ℝ) → ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)) = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
17	7, 16	eqtrd 2774	. . . . . 6 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
18		eqid 2739	. . . . . . . 8 ⊢ {1, 2} = {1, 2}
19		rrx2xpreen.r	. . . . . . . 8 ⊢ 𝑅 = (ℝ ↑_m {1, 2})
20	18, 19	prelrrx2 49204	. . . . . . 7 ⊢ (((1^st ‘𝑧) ∈ ℝ ∧ (2^nd ‘𝑧) ∈ ℝ) → {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} ∈ 𝑅)
21	8, 9, 20	syl2anc 590	. . . . . 6 ⊢ (𝑧 ∈ (ℝ × ℝ) → {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} ∈ 𝑅)
22	17, 21	eqeltrd 2839	. . . . 5 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) ∈ 𝑅)
23	22	rgen 3055	. . . 4 ⊢ ∀𝑧 ∈ (ℝ × ℝ)(𝐹‘𝑧) ∈ 𝑅
24		ffnfv 7060	. . . 4 ⊢ (𝐹:(ℝ × ℝ)⟶𝑅 ↔ (𝐹 Fn (ℝ × ℝ) ∧ ∀𝑧 ∈ (ℝ × ℝ)(𝐹‘𝑧) ∈ 𝑅))
25	3, 23, 24	mpbir2an 717	. . 3 ⊢ 𝐹:(ℝ × ℝ)⟶𝑅
26		opex 5403	. . . . . . . 8 ⊢ ⟨1, (1^st ‘𝑧)⟩ ∈ V
27		opex 5403	. . . . . . . 8 ⊢ ⟨2, (2^nd ‘𝑧)⟩ ∈ V
28		opex 5403	. . . . . . . 8 ⊢ ⟨1, (1^st ‘𝑤)⟩ ∈ V
29		opex 5403	. . . . . . . 8 ⊢ ⟨2, (2^nd ‘𝑤)⟩ ∈ V
30	26, 27, 28, 29	preq12b 4781	. . . . . . 7 ⊢ ({⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩} ↔ ((⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ∧ ⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩) ∨ (⟨1, (1^st ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ ∧ ⟨2, (2^nd ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩)))
31		1ex 11131	. . . . . . . . . . . 12 ⊢ 1 ∈ V
32		fvex 6840	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑧) ∈ V
33	31, 32	opth 5416	. . . . . . . . . . 11 ⊢ (⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ↔ (1 = 1 ∧ (1^st ‘𝑧) = (1^st ‘𝑤)))
34	33	simprbi 498	. . . . . . . . . 10 ⊢ (⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ → (1^st ‘𝑧) = (1^st ‘𝑤))
35		2ex 12249	. . . . . . . . . . . 12 ⊢ 2 ∈ V
36		fvex 6840	. . . . . . . . . . . 12 ⊢ (2^nd ‘𝑧) ∈ V
37	35, 36	opth 5416	. . . . . . . . . . 11 ⊢ (⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ ↔ (2 = 2 ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤)))
38	37	simprbi 498	. . . . . . . . . 10 ⊢ (⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ → (2^nd ‘𝑧) = (2^nd ‘𝑤))
39	34, 38	anim12i 619	. . . . . . . . 9 ⊢ ((⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ∧ ⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤)))
40	39	a1d 25	. . . . . . . 8 ⊢ ((⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ∧ ⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩) → ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
41	31, 32	opth 5416	. . . . . . . . 9 ⊢ (⟨1, (1^st ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ ↔ (1 = 2 ∧ (1^st ‘𝑧) = (2^nd ‘𝑤)))
42	35, 36	opth 5416	. . . . . . . . 9 ⊢ (⟨2, (2^nd ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ↔ (2 = 1 ∧ (2^nd ‘𝑧) = (1^st ‘𝑤)))
43		1ne2 12375	. . . . . . . . . . 11 ⊢ 1 ≠ 2
44		eqneqall 2945	. . . . . . . . . . 11 ⊢ (1 = 2 → (1 ≠ 2 → ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤)))))
45	43, 44	mpi 20	. . . . . . . . . 10 ⊢ (1 = 2 → ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
46	45	ad2antrr 732	. . . . . . . . 9 ⊢ (((1 = 2 ∧ (1^st ‘𝑧) = (2^nd ‘𝑤)) ∧ (2 = 1 ∧ (2^nd ‘𝑧) = (1^st ‘𝑤))) → ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
47	41, 42, 46	syl2anb 604	. . . . . . . 8 ⊢ ((⟨1, (1^st ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ ∧ ⟨2, (2^nd ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩) → ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
48	40, 47	jaoi 863	. . . . . . 7 ⊢ (((⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ∧ ⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩) ∨ (⟨1, (1^st ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ ∧ ⟨2, (2^nd ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩)) → ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
49	30, 48	sylbi 218	. . . . . 6 ⊢ ({⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩} → ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
50	49	com12 32	. . . . 5 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ({⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩} → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
51		1st2nd2 7970	. . . . . . . . 9 ⊢ (𝑤 ∈ (ℝ × ℝ) → 𝑤 = ⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩)
52	51	fveq2d 6831	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (𝐹‘𝑤) = (𝐹‘⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩))
53		df-ov 7359	. . . . . . . 8 ⊢ ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)) = (𝐹‘⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩)
54	52, 53	eqtr4di 2792	. . . . . . 7 ⊢ (𝑤 ∈ (ℝ × ℝ) → (𝐹‘𝑤) = ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)))
55		xp1st 7963	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (1^st ‘𝑤) ∈ ℝ)
56		xp2nd 7964	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (2^nd ‘𝑤) ∈ ℝ)
57		opeq2 4805	. . . . . . . . . 10 ⊢ (𝑥 = (1^st ‘𝑤) → ⟨1, 𝑥⟩ = ⟨1, (1^st ‘𝑤)⟩)
58	57	preq1d 4671	. . . . . . . . 9 ⊢ (𝑥 = (1^st ‘𝑤) → {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, 𝑦⟩})
59		opeq2 4805	. . . . . . . . . 10 ⊢ (𝑦 = (2^nd ‘𝑤) → ⟨2, 𝑦⟩ = ⟨2, (2^nd ‘𝑤)⟩)
60	59	preq2d 4672	. . . . . . . . 9 ⊢ (𝑦 = (2^nd ‘𝑤) → {⟨1, (1^st ‘𝑤)⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
61		prex 5367	. . . . . . . . 9 ⊢ {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩} ∈ V
62	58, 60, 1, 61	ovmpo 7516	. . . . . . . 8 ⊢ (((1^st ‘𝑤) ∈ ℝ ∧ (2^nd ‘𝑤) ∈ ℝ) → ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)) = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
63	55, 56, 62	syl2anc 590	. . . . . . 7 ⊢ (𝑤 ∈ (ℝ × ℝ) → ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)) = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
64	54, 63	eqtrd 2774	. . . . . 6 ⊢ (𝑤 ∈ (ℝ × ℝ) → (𝐹‘𝑤) = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
65	17, 64	eqeqan12d 2753	. . . . 5 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩}))
66	4, 51	eqeqan12d 2753	. . . . . 6 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ = ⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩))
67	32, 36	opth 5416	. . . . . 6 ⊢ (⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ = ⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩ ↔ ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤)))
68	66, 67	bitrdi 288	. . . . 5 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
69	50, 65, 68	3imtr4d 295	. . . 4 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
70	69	rgen2 3179	. . 3 ⊢ ∀𝑧 ∈ (ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)
71		dff13 7198	. . 3 ⊢ (𝐹:(ℝ × ℝ)–1-1→𝑅 ↔ (𝐹:(ℝ × ℝ)⟶𝑅 ∧ ∀𝑧 ∈ (ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)))
72	25, 70, 71	mpbir2an 717	. 2 ⊢ 𝐹:(ℝ × ℝ)–1-1→𝑅
73	19	eleq2i 2831	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑅 ↔ 𝑤 ∈ (ℝ ↑_m {1, 2}))
74		reex 11120	. . . . . . . . 9 ⊢ ℝ ∈ V
75		prex 5367	. . . . . . . . 9 ⊢ {1, 2} ∈ V
76	74, 75	elmap 8809	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ ↑_m {1, 2}) ↔ 𝑤:{1, 2}⟶ℝ)
77		1re 11135	. . . . . . . . 9 ⊢ 1 ∈ ℝ
78		2re 12246	. . . . . . . . 9 ⊢ 2 ∈ ℝ
79		fpr2g 7155	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑤:{1, 2}⟶ℝ ↔ ((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩})))
80	77, 78, 79	mp2an 698	. . . . . . . 8 ⊢ (𝑤:{1, 2}⟶ℝ ↔ ((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}))
81	73, 76, 80	3bitri 298	. . . . . . 7 ⊢ (𝑤 ∈ 𝑅 ↔ ((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}))
82		opeq2 4805	. . . . . . . . . 10 ⊢ (𝑢 = (𝑤‘1) → ⟨1, 𝑢⟩ = ⟨1, (𝑤‘1)⟩)
83	82	preq1d 4671	. . . . . . . . 9 ⊢ (𝑢 = (𝑤‘1) → {⟨1, 𝑢⟩, ⟨2, 𝑣⟩} = {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩})
84	83	eqeq2d 2750	. . . . . . . 8 ⊢ (𝑢 = (𝑤‘1) → (𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩} ↔ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩}))
85		opeq2 4805	. . . . . . . . . 10 ⊢ (𝑣 = (𝑤‘2) → ⟨2, 𝑣⟩ = ⟨2, (𝑤‘2)⟩)
86	85	preq2d 4672	. . . . . . . . 9 ⊢ (𝑣 = (𝑤‘2) → {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩} = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩})
87	86	eqeq2d 2750	. . . . . . . 8 ⊢ (𝑣 = (𝑤‘2) → (𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩} ↔ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}))
88	84, 87	rspc2ev 3573	. . . . . . 7 ⊢ (((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}) → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
89	81, 88	sylbi 218	. . . . . 6 ⊢ (𝑤 ∈ 𝑅 → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
90		opeq2 4805	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → ⟨1, 𝑥⟩ = ⟨1, 𝑢⟩)
91	90	preq1d 4671	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} = {⟨1, 𝑢⟩, ⟨2, 𝑦⟩})
92		opeq2 4805	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → ⟨2, 𝑦⟩ = ⟨2, 𝑣⟩)
93	92	preq2d 4672	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → {⟨1, 𝑢⟩, ⟨2, 𝑦⟩} = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
94		prex 5367	. . . . . . . . 9 ⊢ {⟨1, 𝑢⟩, ⟨2, 𝑣⟩} ∈ V
95	91, 93, 1, 94	ovmpo 7516	. . . . . . . 8 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢𝐹𝑣) = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
96	95	eqeq2d 2750	. . . . . . 7 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑤 = (𝑢𝐹𝑣) ↔ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩}))
97	96	2rexbiia 3200	. . . . . 6 ⊢ (∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
98	89, 97	sylibr 235	. . . . 5 ⊢ (𝑤 ∈ 𝑅 → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣))
99		fveq2 6827	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝐹‘𝑧) = (𝐹‘⟨𝑢, 𝑣⟩))
100		df-ov 7359	. . . . . . . 8 ⊢ (𝑢𝐹𝑣) = (𝐹‘⟨𝑢, 𝑣⟩)
101	99, 100	eqtr4di 2792	. . . . . . 7 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝐹‘𝑧) = (𝑢𝐹𝑣))
102	101	eqeq2d 2750	. . . . . 6 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑤 = (𝐹‘𝑧) ↔ 𝑤 = (𝑢𝐹𝑣)))
103	102	rexxp 5784	. . . . 5 ⊢ (∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣))
104	98, 103	sylibr 235	. . . 4 ⊢ (𝑤 ∈ 𝑅 → ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧))
105	104	rgen 3055	. . 3 ⊢ ∀𝑤 ∈ 𝑅 ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧)
106		dffo3 7043	. . 3 ⊢ (𝐹:(ℝ × ℝ)–onto→𝑅 ↔ (𝐹:(ℝ × ℝ)⟶𝑅 ∧ ∀𝑤 ∈ 𝑅 ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧)))
107	25, 105, 106	mpbir2an 717	. 2 ⊢ 𝐹:(ℝ × ℝ)–onto→𝑅
108		df-f1o 6492	. 2 ⊢ (𝐹:(ℝ × ℝ)–1-1-onto→𝑅 ↔ (𝐹:(ℝ × ℝ)–1-1→𝑅 ∧ 𝐹:(ℝ × ℝ)–onto→𝑅))
109	72, 107, 108	mpbir2an 717	1 ⊢ 𝐹:(ℝ × ℝ)–1-1-onto→𝑅

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 {cpr 4557 ⟨cop 4561 × cxp 5616 Fn wfn 6480 ⟶wf 6481 –1-1→wf1 6482 –onto→wfo 6483 –1-1-onto→wf1o 6484 ‘cfv 6485 (class class class)co 7356 ∈ cmpo 7358 1^st c1st 7929 2^nd c2nd 7930 ↑_m cmap 8763 ℝcr 11028 1c1 11030 2c2 12227

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-id 5513 df-po 5526 df-so 5527 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-1st 7931 df-2nd 7932 df-er 8633 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-2 12235

This theorem is referenced by: rrx2xpreen 49210 rrx2plordisom 49214

W3C validator