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	⊢ 𝑅 = ( ℝ ↑_m { 1 , 2 } )
	rrx2xpref1o.1	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } )
Assertion	rrx2xpref1o	⊢ 𝐹 : ( ℝ × ℝ ) –1-1-onto→ 𝑅

Proof

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

Metamath Proof Explorer

Theorem rrx2xpref1o

Proof