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 48711

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 5395	. . . . 5 ⊢ {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} ∈ V
3	1, 2	fnmpoi 8052	. . . 4 ⊢ 𝐹 Fn (ℝ × ℝ)
4		1st2nd2 8010	. . . . . . . . 9 ⊢ (𝑧 ∈ (ℝ × ℝ) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
5	4	fveq2d 6865	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = (𝐹‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
6		df-ov 7393	. . . . . . . 8 ⊢ ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)) = (𝐹‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
7	5, 6	eqtr4di 2783	. . . . . . 7 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)))
8		xp1st 8003	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (1^st ‘𝑧) ∈ ℝ)
9		xp2nd 8004	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (2^nd ‘𝑧) ∈ ℝ)
10		opeq2 4841	. . . . . . . . . 10 ⊢ (𝑥 = (1^st ‘𝑧) → ⟨1, 𝑥⟩ = ⟨1, (1^st ‘𝑧)⟩)
11	10	preq1d 4706	. . . . . . . . 9 ⊢ (𝑥 = (1^st ‘𝑧) → {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑧)⟩, ⟨2, 𝑦⟩})
12		opeq2 4841	. . . . . . . . . 10 ⊢ (𝑦 = (2^nd ‘𝑧) → ⟨2, 𝑦⟩ = ⟨2, (2^nd ‘𝑧)⟩)
13	12	preq2d 4707	. . . . . . . . 9 ⊢ (𝑦 = (2^nd ‘𝑧) → {⟨1, (1^st ‘𝑧)⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
14		prex 5395	. . . . . . . . 9 ⊢ {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} ∈ V
15	11, 13, 1, 14	ovmpo 7552	. . . . . . . 8 ⊢ (((1^st ‘𝑧) ∈ ℝ ∧ (2^nd ‘𝑧) ∈ ℝ) → ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)) = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
16	8, 9, 15	syl2anc 584	. . . . . . 7 ⊢ (𝑧 ∈ (ℝ × ℝ) → ((1^st ‘𝑧)𝐹(2^nd ‘𝑧)) = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
17	7, 16	eqtrd 2765	. . . . . 6 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩})
18		eqid 2730	. . . . . . . 8 ⊢ {1, 2} = {1, 2}
19		rrx2xpreen.r	. . . . . . . 8 ⊢ 𝑅 = (ℝ ↑_m {1, 2})
20	18, 19	prelrrx2 48706	. . . . . . 7 ⊢ (((1^st ‘𝑧) ∈ ℝ ∧ (2^nd ‘𝑧) ∈ ℝ) → {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} ∈ 𝑅)
21	8, 9, 20	syl2anc 584	. . . . . 6 ⊢ (𝑧 ∈ (ℝ × ℝ) → {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} ∈ 𝑅)
22	17, 21	eqeltrd 2829	. . . . 5 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) ∈ 𝑅)
23	22	rgen 3047	. . . 4 ⊢ ∀𝑧 ∈ (ℝ × ℝ)(𝐹‘𝑧) ∈ 𝑅
24		ffnfv 7094	. . . 4 ⊢ (𝐹:(ℝ × ℝ)⟶𝑅 ↔ (𝐹 Fn (ℝ × ℝ) ∧ ∀𝑧 ∈ (ℝ × ℝ)(𝐹‘𝑧) ∈ 𝑅))
25	3, 23, 24	mpbir2an 711	. . 3 ⊢ 𝐹:(ℝ × ℝ)⟶𝑅
26		opex 5427	. . . . . . . 8 ⊢ ⟨1, (1^st ‘𝑧)⟩ ∈ V
27		opex 5427	. . . . . . . 8 ⊢ ⟨2, (2^nd ‘𝑧)⟩ ∈ V
28		opex 5427	. . . . . . . 8 ⊢ ⟨1, (1^st ‘𝑤)⟩ ∈ V
29		opex 5427	. . . . . . . 8 ⊢ ⟨2, (2^nd ‘𝑤)⟩ ∈ V
30	26, 27, 28, 29	preq12b 4817	. . . . . . 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 11177	. . . . . . . . . . . 12 ⊢ 1 ∈ V
32		fvex 6874	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑧) ∈ V
33	31, 32	opth 5439	. . . . . . . . . . 11 ⊢ (⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ↔ (1 = 1 ∧ (1^st ‘𝑧) = (1^st ‘𝑤)))
34	33	simprbi 496	. . . . . . . . . 10 ⊢ (⟨1, (1^st ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ → (1^st ‘𝑧) = (1^st ‘𝑤))
35		2ex 12270	. . . . . . . . . . . 12 ⊢ 2 ∈ V
36		fvex 6874	. . . . . . . . . . . 12 ⊢ (2^nd ‘𝑧) ∈ V
37	35, 36	opth 5439	. . . . . . . . . . 11 ⊢ (⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ ↔ (2 = 2 ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤)))
38	37	simprbi 496	. . . . . . . . . 10 ⊢ (⟨2, (2^nd ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ → (2^nd ‘𝑧) = (2^nd ‘𝑤))
39	34, 38	anim12i 613	. . . . . . . . 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 5439	. . . . . . . . 9 ⊢ (⟨1, (1^st ‘𝑧)⟩ = ⟨2, (2^nd ‘𝑤)⟩ ↔ (1 = 2 ∧ (1^st ‘𝑧) = (2^nd ‘𝑤)))
42	35, 36	opth 5439	. . . . . . . . 9 ⊢ (⟨2, (2^nd ‘𝑧)⟩ = ⟨1, (1^st ‘𝑤)⟩ ↔ (2 = 1 ∧ (2^nd ‘𝑧) = (1^st ‘𝑤)))
43		1ne2 12396	. . . . . . . . . . 11 ⊢ 1 ≠ 2
44		eqneqall 2937	. . . . . . . . . . 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 726	. . . . . . . . 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 598	. . . . . . . 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 857	. . . . . . 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 217	. . . . . 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 8010	. . . . . . . . 9 ⊢ (𝑤 ∈ (ℝ × ℝ) → 𝑤 = ⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩)
52	51	fveq2d 6865	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (𝐹‘𝑤) = (𝐹‘⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩))
53		df-ov 7393	. . . . . . . 8 ⊢ ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)) = (𝐹‘⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩)
54	52, 53	eqtr4di 2783	. . . . . . 7 ⊢ (𝑤 ∈ (ℝ × ℝ) → (𝐹‘𝑤) = ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)))
55		xp1st 8003	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (1^st ‘𝑤) ∈ ℝ)
56		xp2nd 8004	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (2^nd ‘𝑤) ∈ ℝ)
57		opeq2 4841	. . . . . . . . . 10 ⊢ (𝑥 = (1^st ‘𝑤) → ⟨1, 𝑥⟩ = ⟨1, (1^st ‘𝑤)⟩)
58	57	preq1d 4706	. . . . . . . . 9 ⊢ (𝑥 = (1^st ‘𝑤) → {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, 𝑦⟩})
59		opeq2 4841	. . . . . . . . . 10 ⊢ (𝑦 = (2^nd ‘𝑤) → ⟨2, 𝑦⟩ = ⟨2, (2^nd ‘𝑤)⟩)
60	59	preq2d 4707	. . . . . . . . 9 ⊢ (𝑦 = (2^nd ‘𝑤) → {⟨1, (1^st ‘𝑤)⟩, ⟨2, 𝑦⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
61		prex 5395	. . . . . . . . 9 ⊢ {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩} ∈ V
62	58, 60, 1, 61	ovmpo 7552	. . . . . . . 8 ⊢ (((1^st ‘𝑤) ∈ ℝ ∧ (2^nd ‘𝑤) ∈ ℝ) → ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)) = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
63	55, 56, 62	syl2anc 584	. . . . . . 7 ⊢ (𝑤 ∈ (ℝ × ℝ) → ((1^st ‘𝑤)𝐹(2^nd ‘𝑤)) = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
64	54, 63	eqtrd 2765	. . . . . 6 ⊢ (𝑤 ∈ (ℝ × ℝ) → (𝐹‘𝑤) = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩})
65	17, 64	eqeqan12d 2744	. . . . 5 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ {⟨1, (1^st ‘𝑧)⟩, ⟨2, (2^nd ‘𝑧)⟩} = {⟨1, (1^st ‘𝑤)⟩, ⟨2, (2^nd ‘𝑤)⟩}))
66	4, 51	eqeqan12d 2744	. . . . . 6 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ = ⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩))
67	32, 36	opth 5439	. . . . . 6 ⊢ (⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ = ⟨(1^st ‘𝑤), (2^nd ‘𝑤)⟩ ↔ ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤)))
68	66, 67	bitrdi 287	. . . . 5 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ((1^st ‘𝑧) = (1^st ‘𝑤) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑤))))
69	50, 65, 68	3imtr4d 294	. . . 4 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
70	69	rgen2 3178	. . 3 ⊢ ∀𝑧 ∈ (ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)
71		dff13 7232	. . 3 ⊢ (𝐹:(ℝ × ℝ)–1-1→𝑅 ↔ (𝐹:(ℝ × ℝ)⟶𝑅 ∧ ∀𝑧 ∈ (ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)))
72	25, 70, 71	mpbir2an 711	. 2 ⊢ 𝐹:(ℝ × ℝ)–1-1→𝑅
73	19	eleq2i 2821	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑅 ↔ 𝑤 ∈ (ℝ ↑_m {1, 2}))
74		reex 11166	. . . . . . . . 9 ⊢ ℝ ∈ V
75		prex 5395	. . . . . . . . 9 ⊢ {1, 2} ∈ V
76	74, 75	elmap 8847	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ ↑_m {1, 2}) ↔ 𝑤:{1, 2}⟶ℝ)
77		1re 11181	. . . . . . . . 9 ⊢ 1 ∈ ℝ
78		2re 12267	. . . . . . . . 9 ⊢ 2 ∈ ℝ
79		fpr2g 7188	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑤:{1, 2}⟶ℝ ↔ ((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩})))
80	77, 78, 79	mp2an 692	. . . . . . . 8 ⊢ (𝑤:{1, 2}⟶ℝ ↔ ((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}))
81	73, 76, 80	3bitri 297	. . . . . . 7 ⊢ (𝑤 ∈ 𝑅 ↔ ((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}))
82		opeq2 4841	. . . . . . . . . 10 ⊢ (𝑢 = (𝑤‘1) → ⟨1, 𝑢⟩ = ⟨1, (𝑤‘1)⟩)
83	82	preq1d 4706	. . . . . . . . 9 ⊢ (𝑢 = (𝑤‘1) → {⟨1, 𝑢⟩, ⟨2, 𝑣⟩} = {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩})
84	83	eqeq2d 2741	. . . . . . . 8 ⊢ (𝑢 = (𝑤‘1) → (𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩} ↔ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩}))
85		opeq2 4841	. . . . . . . . . 10 ⊢ (𝑣 = (𝑤‘2) → ⟨2, 𝑣⟩ = ⟨2, (𝑤‘2)⟩)
86	85	preq2d 4707	. . . . . . . . 9 ⊢ (𝑣 = (𝑤‘2) → {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩} = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩})
87	86	eqeq2d 2741	. . . . . . . 8 ⊢ (𝑣 = (𝑤‘2) → (𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, 𝑣⟩} ↔ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}))
88	84, 87	rspc2ev 3604	. . . . . . 7 ⊢ (((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧ 𝑤 = {⟨1, (𝑤‘1)⟩, ⟨2, (𝑤‘2)⟩}) → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
89	81, 88	sylbi 217	. . . . . 6 ⊢ (𝑤 ∈ 𝑅 → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
90		opeq2 4841	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → ⟨1, 𝑥⟩ = ⟨1, 𝑢⟩)
91	90	preq1d 4706	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → {⟨1, 𝑥⟩, ⟨2, 𝑦⟩} = {⟨1, 𝑢⟩, ⟨2, 𝑦⟩})
92		opeq2 4841	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → ⟨2, 𝑦⟩ = ⟨2, 𝑣⟩)
93	92	preq2d 4707	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → {⟨1, 𝑢⟩, ⟨2, 𝑦⟩} = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
94		prex 5395	. . . . . . . . 9 ⊢ {⟨1, 𝑢⟩, ⟨2, 𝑣⟩} ∈ V
95	91, 93, 1, 94	ovmpo 7552	. . . . . . . 8 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢𝐹𝑣) = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
96	95	eqeq2d 2741	. . . . . . 7 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑤 = (𝑢𝐹𝑣) ↔ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩}))
97	96	2rexbiia 3199	. . . . . 6 ⊢ (∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {⟨1, 𝑢⟩, ⟨2, 𝑣⟩})
98	89, 97	sylibr 234	. . . . 5 ⊢ (𝑤 ∈ 𝑅 → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣))
99		fveq2 6861	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝐹‘𝑧) = (𝐹‘⟨𝑢, 𝑣⟩))
100		df-ov 7393	. . . . . . . 8 ⊢ (𝑢𝐹𝑣) = (𝐹‘⟨𝑢, 𝑣⟩)
101	99, 100	eqtr4di 2783	. . . . . . 7 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝐹‘𝑧) = (𝑢𝐹𝑣))
102	101	eqeq2d 2741	. . . . . 6 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑤 = (𝐹‘𝑧) ↔ 𝑤 = (𝑢𝐹𝑣)))
103	102	rexxp 5809	. . . . 5 ⊢ (∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣))
104	98, 103	sylibr 234	. . . 4 ⊢ (𝑤 ∈ 𝑅 → ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧))
105	104	rgen 3047	. . 3 ⊢ ∀𝑤 ∈ 𝑅 ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧)
106		dffo3 7077	. . 3 ⊢ (𝐹:(ℝ × ℝ)–onto→𝑅 ↔ (𝐹:(ℝ × ℝ)⟶𝑅 ∧ ∀𝑤 ∈ 𝑅 ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧)))
107	25, 105, 106	mpbir2an 711	. 2 ⊢ 𝐹:(ℝ × ℝ)–onto→𝑅
108		df-f1o 6521	. 2 ⊢ (𝐹:(ℝ × ℝ)–1-1-onto→𝑅 ↔ (𝐹:(ℝ × ℝ)–1-1→𝑅 ∧ 𝐹:(ℝ × ℝ)–onto→𝑅))
109	72, 107, 108	mpbir2an 711	1 ⊢ 𝐹:(ℝ × ℝ)–1-1-onto→𝑅

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 {cpr 4594 ⟨cop 4598 × cxp 5639 Fn wfn 6509 ⟶wf 6510 –1-1→wf1 6511 –onto→wfo 6512 –1-1-onto→wf1o 6513 ‘cfv 6514 (class class class)co 7390 ∈ cmpo 7392 1^st c1st 7969 2^nd c2nd 7970 ↑_m cmap 8802 ℝcr 11074 1c1 11076 2c2 12248

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-po 5549 df-so 5550 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-1st 7971 df-2nd 7972 df-er 8674 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-2 12256

This theorem is referenced by: rrx2xpreen 48712 rrx2plordisom 48716

W3C validator