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 49518

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 5409	. . . . 5 ⊢ {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} ∈ V
3	1, 2	fnmpoi 8063	. . . 4 ⊢ 𝐹 Fn (ℝ × ℝ)
4		1st2nd2 8021	. . . . . . . . 9 ⊢ (𝑧 ∈ (ℝ × ℝ) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
5	4	fveq2d 6885	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = (𝐹‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
6		df-ov 7413	. . . . . . . 8 ⊢ ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)) = (𝐹‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
7	5, 6	eqtr4di 2816	. . . . . . 7 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)))
8		xp1st 8014	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (1^st ‘𝑧) ∈ ℝ)
9		xp2nd 8015	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (2^nd ‘𝑧) ∈ ℝ)
10		opeq2 4839	. . . . . . . . . 10 ⊢ (𝑥 = (1^st ‘𝑧) → ⟨1, 𝑥⟩ = ⟨1, (1^st ‘𝑧)⟩)
11	10	preq1d 4705	. . . . . . . . 9 ⊢ (𝑥 = (1^st ‘𝑧) → {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑧)⟩, ⟨2, 𝑦⟩})
12		opeq2 4839	. . . . . . . . . 10 ⊢ (𝑦 = (2^nd ‘𝑧) → ⟨2, 𝑦⟩ = ⟨2, (2^nd ‘𝑧)⟩)
13	12	preq2d 4706	. . . . . . . . 9 ⊢ (𝑦 = (2^nd ‘𝑧) → {⟨1, (1^st ‘𝑧)⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
14		prex 5409	. . . . . . . . 9 ⊢ {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} ∈ V
15	11, 13, 1, 14	ovmpo 7570	. . . . . . . 8 ⊢ (((1^st ‘𝑧) ∈ ℝ ∧ (2^nd ‘𝑧) ∈ ℝ) → ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)) = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
16	8, 9, 15	syl2anc 595	. . . . . . 7 ⊢ (𝑧 ∈ (ℝ × ℝ) → ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)) = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
17	7, 16	eqtrd 2798	. . . . . 6 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
18		eqid 2763	. . . . . . . 8 ⊢ {1, 2} = {1, 2}
19		rrx2xpreen.r	. . . . . . . 8 ⊢ 𝑅 = (ℝ ↑_m {1, 2})
20	18, 19	prelrrx2 49513	. . . . . . 7 ⊢ (((1^st ‘𝑧) ∈ ℝ ∧ (2^nd ‘𝑧) ∈ ℝ) → {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} ∈ 𝑅)
21	8, 9, 20	syl2anc 595	. . . . . 6 ⊢ (𝑧 ∈ (ℝ × ℝ) → {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} ∈ 𝑅)
22	17, 21	eqeltrd 2863	. . . . 5 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) ∈ 𝑅)
23	22	rgen 3081	. . . 4 ⊢ ∀𝑧 ∈ (ℝ × ℝ)(𝐹‘𝑧) ∈ 𝑅
24		ffnfv 7114	. . . 4 ⊢ (𝐹:(ℝ × ℝ)⟶𝑅 ↔ (𝐹 Fn (ℝ × ℝ) ∧ ∀𝑧 ∈ (ℝ × ℝ)(𝐹‘𝑧) ∈ 𝑅))
25	3, 23, 24	mpbir2an 723	. . 3 ⊢ 𝐹:(ℝ × ℝ)⟶𝑅
26		opex 5445	. . . . . . . 8 ⊢ ⟨1, (1^st ‘𝑧)⟩ ∈ V
27		opex 5445	. . . . . . . 8 ⊢ ⟨2, (2^nd ‘𝑧)⟩ ∈ V
28		opex 5445	. . . . . . . 8 ⊢ ⟨1, (1^st ‘𝑤)⟩ ∈ V
29		opex 5445	. . . . . . . 8 ⊢ ⟨2, (2^nd ‘𝑤)⟩ ∈ V
30	26, 27, 28, 29	preq12b 4815	. . . . . . 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 11198	. . . . . . . . . . . 12 ⊢ 1 ∈ V
32		fvex 6894	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑧) ∈ V
33	31, 32	opth 5458	. . . . . . . . . . 11 ⊢ (⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ↔ (1 = 1 ∧ (1^st ‘𝑧) = (1^st ‘𝑤)))
34	33	simprbi 502	. . . . . . . . . 10 ⊢ (⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ → (1^st ‘𝑧) = (1^st ‘𝑤))
35		2ex 12313	. . . . . . . . . . . 12 ⊢ 2 ∈ V
36		fvex 6894	. . . . . . . . . . . 12 ⊢ (2^nd ‘𝑧) ∈ V
37	35, 36	opth 5458	. . . . . . . . . . 11 ⊢ (⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ ↔ (2 = 2 ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤)))
38	37	simprbi 502	. . . . . . . . . 10 ⊢ (⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ → (2^nd ‘𝑧) = (2^nd ‘𝑤))
39	34, 38	anim12i 624	. . . . . . . . 9 ⊢ ((⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ∧ ⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤)))
40	39	a1d 26	. . . . . . . 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 5458	. . . . . . . . 9 ⊢ (⟨1, (1^st ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ ↔ (1 = 2 ∧ (1^st ‘𝑧) = (2^nd ‘𝑤)))
42	35, 36	opth 5458	. . . . . . . . 9 ⊢ (⟨2, (2^nd ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ↔ (2 = 1 ∧ (2^nd ‘𝑧) = (1^st ‘𝑤)))
43		1ne2 12446	. . . . . . . . . . 11 ⊢ 1 ≠ 2
44		eqneqall 2969	. . . . . . . . . . 11 ⊢ (1 = 2 → (1 ≠ 2 → ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤)))))
45	43, 44	mpi 21	. . . . . . . . . 10 ⊢ (1 = 2 → ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
46	45	ad2antrr 738	. . . . . . . . 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 609	. . . . . . . 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 870	. . . . . . 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 220	. . . . . 6 ⊢ ({⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩} → ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
50	49	com12 33	. . . . 5 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ({⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩} → ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
51		1st2nd2 8021	. . . . . . . . 9 ⊢ (𝑤 ∈ (ℝ × ℝ) → 𝑤 = ⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩)
52	51	fveq2d 6885	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (𝐹‘𝑤) = (𝐹‘⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩))
53		df-ov 7413	. . . . . . . 8 ⊢ ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)) = (𝐹‘⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩)
54	52, 53	eqtr4di 2816	. . . . . . 7 ⊢ (𝑤 ∈ (ℝ × ℝ) → (𝐹‘𝑤) = ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)))
55		xp1st 8014	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (1^st ‘𝑤) ∈ ℝ)
56		xp2nd 8015	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (2^nd ‘𝑤) ∈ ℝ)
57		opeq2 4839	. . . . . . . . . 10 ⊢ (𝑥 = (1^st ‘𝑤) → ⟨1, 𝑥⟩ = ⟨1, (1^st ‘𝑤)⟩)
58	57	preq1d 4705	. . . . . . . . 9 ⊢ (𝑥 = (1^st ‘𝑤) → {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, 𝑦⟩})
59		opeq2 4839	. . . . . . . . . 10 ⊢ (𝑦 = (2^nd ‘𝑤) → ⟨2, 𝑦⟩ = ⟨2, (2^nd ‘𝑤)⟩)
60	59	preq2d 4706	. . . . . . . . 9 ⊢ (𝑦 = (2^nd ‘𝑤) → {⟨1, (1^st ‘𝑤)⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
61		prex 5409	. . . . . . . . 9 ⊢ {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩} ∈ V
62	58, 60, 1, 61	ovmpo 7570	. . . . . . . 8 ⊢ (((1^st ‘𝑤) ∈ ℝ ∧ (2^nd ‘𝑤) ∈ ℝ) → ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)) = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
63	55, 56, 62	syl2anc 595	. . . . . . 7 ⊢ (𝑤 ∈ (ℝ × ℝ) → ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)) = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
64	54, 63	eqtrd 2798	. . . . . 6 ⊢ (𝑤 ∈ (ℝ × ℝ) → (𝐹‘𝑤) = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
65	17, 64	eqeqan12d 2777	. . . . 5 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩}))
66	4, 51	eqeqan12d 2777	. . . . . 6 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ = ⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩))
67	32, 36	opth 5458	. . . . . 6 ⊢ (⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ = ⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩ ↔ ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤)))
68	66, 67	bitrdi 290	. . . . 5 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
69	50, 65, 68	3imtr4d 297	. . . 4 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
70	69	rgen2 3205	. . 3 ⊢ ∀𝑧 ∈ (ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)
71		dff13 7252	. . 3 ⊢ (𝐹:(ℝ × ℝ)–1-1→𝑅 ↔ (𝐹:(ℝ × ℝ)⟶𝑅 ∧ ∀𝑧 ∈ (ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)))
72	25, 70, 71	mpbir2an 723	. 2 ⊢ 𝐹:(ℝ × ℝ)–1-1→𝑅
73	19	eleq2i 2855	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑅 ↔ 𝑤 ∈ (ℝ ↑_m {1, 2}))
74		reex 11186	. . . . . . . . 9 ⊢ ℝ ∈ V
75		prex 5409	. . . . . . . . 9 ⊢ {1, 2} ∈ V
76	74, 75	elmap 8865	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ ↑_m {1, 2}) ↔ 𝑤:{1, 2}⟶ℝ)
77		1re 11203	. . . . . . . . 9 ⊢ 1 ∈ ℝ
78		2re 12310	. . . . . . . . 9 ⊢ 2 ∈ ℝ
79		fpr2g 7209	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑤:{1, 2}⟶ℝ ↔ ((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩})))
80	77, 78, 79	mp2an 704	. . . . . . . 8 ⊢ (𝑤:{1, 2}⟶ℝ ↔ ((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}))
81	73, 76, 80	3bitri 300	. . . . . . 7 ⊢ (𝑤 ∈ 𝑅 ↔ ((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}))
82		opeq2 4839	. . . . . . . . . 10 ⊢ (𝑢 = (𝑤‘1) → ⟨1, 𝑢⟩ = ⟨1, (𝑤‘1)⟩)
83	82	preq1d 4705	. . . . . . . . 9 ⊢ (𝑢 = (𝑤‘1) → {⟨1, 𝑢⟩, ⟨2, 𝑣⟩} = {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩})
84	83	eqeq2d 2774	. . . . . . . 8 ⊢ (𝑢 = (𝑤‘1) → (𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩} ↔ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩}))
85		opeq2 4839	. . . . . . . . . 10 ⊢ (𝑣 = (𝑤‘2) → ⟨2, 𝑣⟩ = ⟨2, (𝑤‘2)⟩)
86	85	preq2d 4706	. . . . . . . . 9 ⊢ (𝑣 = (𝑤‘2) → {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩} = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩})
87	86	eqeq2d 2774	. . . . . . . 8 ⊢ (𝑣 = (𝑤‘2) → (𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩} ↔ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}))
88	84, 87	rspc2ev 3594	. . . . . . 7 ⊢ (((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}) → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
89	81, 88	sylbi 220	. . . . . 6 ⊢ (𝑤 ∈ 𝑅 → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
90		opeq2 4839	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → ⟨1, 𝑥⟩ = ⟨1, 𝑢⟩)
91	90	preq1d 4705	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} = {⟨1, 𝑢⟩, ⟨2, 𝑦⟩})
92		opeq2 4839	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → ⟨2, 𝑦⟩ = ⟨2, 𝑣⟩)
93	92	preq2d 4706	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → {⟨1, 𝑢⟩, ⟨2, 𝑦⟩} = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
94		prex 5409	. . . . . . . . 9 ⊢ {⟨1, 𝑢⟩, ⟨2, 𝑣⟩} ∈ V
95	91, 93, 1, 94	ovmpo 7570	. . . . . . . 8 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢𝐹𝑣) = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
96	95	eqeq2d 2774	. . . . . . 7 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑤 = (𝑢𝐹𝑣) ↔ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩}))
97	96	2rexbiia 3226	. . . . . 6 ⊢ (∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
98	89, 97	sylibr 237	. . . . 5 ⊢ (𝑤 ∈ 𝑅 → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣))
99		fveq2 6881	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝐹‘𝑧) = (𝐹‘⟨𝑢, 𝑣⟩))
100		df-ov 7413	. . . . . . . 8 ⊢ (𝑢𝐹𝑣) = (𝐹‘⟨𝑢, 𝑣⟩)
101	99, 100	eqtr4di 2816	. . . . . . 7 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝐹‘𝑧) = (𝑢𝐹𝑣))
102	101	eqeq2d 2774	. . . . . 6 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑤 = (𝐹‘𝑧) ↔ 𝑤 = (𝑢𝐹𝑣)))
103	102	rexxp 5828	. . . . 5 ⊢ (∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣))
104	98, 103	sylibr 237	. . . 4 ⊢ (𝑤 ∈ 𝑅 → ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧))
105	104	rgen 3081	. . 3 ⊢ ∀𝑤 ∈ 𝑅 ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧)
106		dffo3 7097	. . 3 ⊢ (𝐹:(ℝ × ℝ)–onto→𝑅 ↔ (𝐹:(ℝ × ℝ)⟶𝑅 ∧ ∀𝑤 ∈ 𝑅 ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧)))
107	25, 105, 106	mpbir2an 723	. 2 ⊢ 𝐹:(ℝ × ℝ)–onto→𝑅
108		df-f1o 6543	. 2 ⊢ (𝐹:(ℝ × ℝ)–1-1-onto→𝑅 ↔ (𝐹:(ℝ × ℝ)–1-1→𝑅 ∧ 𝐹:(ℝ × ℝ)–onto→𝑅))
109	72, 107, 108	mpbir2an 723	1 ⊢ 𝐹:(ℝ × ℝ)–1-1-onto→𝑅

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 {cpr 4591 ⟨cop 4595 × cxp 5659 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 –onto→wfo 6534 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 ∈ cmpo 7412 1^st c1st 7980 2^nd c2nd 7981 ↑_m cmap 8820 ℝcr 11094 1c1 11096 2c2 12290

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-id 5556 df-po 5569 df-so 5570 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-1st 7982 df-2nd 7983 df-er 8690 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-2 12298

This theorem is referenced by: rrx2xpreen 49519 rrx2plordisom 49523

W3C validator