Metamath Proof Explorer

Theorem 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 ( 0 ..^ 2 ) to the real numbers). (Contributed by AV, 12-Mar-2023)

Ref Expression
Hypotheses rrx2xpreen.r ⊢ 𝑅 = ( ℝ ↑m ( 0 ..^ 2 ) )
rrx2xpref1o.1 ⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ )
Assertion rrx2xpref1o 𝐹 : ( ℝ × ℝ ) –1-1-onto→ 𝑅

Proof

Step Hyp Ref Expression
1 rrx2xpreen.r ⊢ 𝑅 = ( ℝ ↑m ( 0 ..^ 2 ) )
2 rrx2xpref1o.1 ⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ )
3 simprl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → 𝑥 ∈ ℝ )
4 simprr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → 𝑦 ∈ ℝ )
5 3 4 s2cld ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ⟨“ 𝑥 𝑦 ”⟩ ∈ Word ℝ )
6 eqid ⊢ ( 0 ..^ 2 ) = ( 0 ..^ 2 )
7 6 1 rrx2pxel ⊢ ( 𝑧 ∈ 𝑅 → ( 𝑧 ‘ 0 ) ∈ ℝ )
8 6 1 rrx2pyel ⊢ ( 𝑧 ∈ 𝑅 → ( 𝑧 ‘ 1 ) ∈ ℝ )
9 7 8 jca ⊢ ( 𝑧 ∈ 𝑅 → ( ( 𝑧 ‘ 0 ) ∈ ℝ ∧ ( 𝑧 ‘ 1 ) ∈ ℝ ) )
10 9 adantl ⊢ ( ( ⊤ ∧ 𝑧 ∈ 𝑅 ) → ( ( 𝑧 ‘ 0 ) ∈ ℝ ∧ ( 𝑧 ‘ 1 ) ∈ ℝ ) )
11 simprl ⊢ ( ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) → ( 𝑧 ‘ 0 ) = 𝑥 )
12 7 adantr ⊢ ( ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) → ( 𝑧 ‘ 0 ) ∈ ℝ )
13 11 12 eqeltrrd ⊢ ( ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) → 𝑥 ∈ ℝ )
14 simprr ⊢ ( ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) → ( 𝑧 ‘ 1 ) = 𝑦 )
15 8 adantr ⊢ ( ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) → ( 𝑧 ‘ 1 ) ∈ ℝ )
16 14 15 eqeltrrd ⊢ ( ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) → 𝑦 ∈ ℝ )
17 13 16 jca ⊢ ( ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) → ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) )
18 17 pm4.71ri ⊢ ( ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) ) )
19 eqcom ⊢ ( 𝑥 = ( 𝑧 ‘ 0 ) ↔ ( 𝑧 ‘ 0 ) = 𝑥 )
20 eqcom ⊢ ( 𝑦 = ( 𝑧 ‘ 1 ) ↔ ( 𝑧 ‘ 1 ) = 𝑦 )
21 19 20 anbi12i ⊢ ( ( 𝑥 = ( 𝑧 ‘ 0 ) ∧ 𝑦 = ( 𝑧 ‘ 1 ) ) ↔ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) )
22 21 anbi2i ⊢ ( ( 𝑧 ∈ 𝑅 ∧ ( 𝑥 = ( 𝑧 ‘ 0 ) ∧ 𝑦 = ( 𝑧 ‘ 1 ) ) ) ↔ ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) )
23 simpl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℝ )
24 simpr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
25 6 1 23 24 prelrrx2bd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 = ⟨“ 𝑥 𝑦 ”⟩ ↔ ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) ) )
26 25 pm5.32i ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 = ⟨“ 𝑥 𝑦 ”⟩ ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑅 ∧ ( ( 𝑧 ‘ 0 ) = 𝑥 ∧ ( 𝑧 ‘ 1 ) = 𝑦 ) ) ) )
27 18 22 26 3bitr4ri ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 = ⟨“ 𝑥 𝑦 ”⟩ ) ↔ ( 𝑧 ∈ 𝑅 ∧ ( 𝑥 = ( 𝑧 ‘ 0 ) ∧ 𝑦 = ( 𝑧 ‘ 1 ) ) ) )
28 27 a1i ⊢ ( ⊤ → ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 = ⟨“ 𝑥 𝑦 ”⟩ ) ↔ ( 𝑧 ∈ 𝑅 ∧ ( 𝑥 = ( 𝑧 ‘ 0 ) ∧ 𝑦 = ( 𝑧 ‘ 1 ) ) ) ) )
29 2 5 10 28 f1od2 ⊢ ( ⊤ → 𝐹 : ( ℝ × ℝ ) –1-1-onto→ 𝑅 )
30 29 mptru ⊢ 𝐹 : ( ℝ × ℝ ) –1-1-onto→ 𝑅