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 { 1 , 2 } to the real numbers). (Contributed by AV, 12-Mar-2023)

Ref Expression
Hypotheses rrx2xpreen.r 
|- R = ( RR ^m { 1 , 2 } )
rrx2xpref1o.1 
|- F = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } )
Assertion rrx2xpref1o 
|- F : ( RR X. RR ) -1-1-onto-> R

Proof

Step Hyp Ref Expression
1 rrx2xpreen.r 
 |-  R = ( RR ^m { 1 , 2 } )
2 rrx2xpref1o.1 
 |-  F = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } )
3 prex 
 |-  { <. 1 , x >. , <. 2 , y >. } e. _V
4 2 3 fnmpoi 
 |-  F Fn ( RR X. RR )
5 1st2nd2 
 |-  ( z e. ( RR X. RR ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
6 5 fveq2d 
 |-  ( z e. ( RR X. RR ) -> ( F ` z ) = ( F ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
7 df-ov 
 |-  ( ( 1st ` z ) F ( 2nd ` z ) ) = ( F ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
8 6 7 eqtr4di 
 |-  ( z e. ( RR X. RR ) -> ( F ` z ) = ( ( 1st ` z ) F ( 2nd ` z ) ) )
9 xp1st 
 |-  ( z e. ( RR X. RR ) -> ( 1st ` z ) e. RR )
10 xp2nd 
 |-  ( z e. ( RR X. RR ) -> ( 2nd ` z ) e. RR )
11 opeq2 
 |-  ( x = ( 1st ` z ) -> <. 1 , x >. = <. 1 , ( 1st ` z ) >. )
12 11 preq1d 
 |-  ( x = ( 1st ` z ) -> { <. 1 , x >. , <. 2 , y >. } = { <. 1 , ( 1st ` z ) >. , <. 2 , y >. } )
13 opeq2 
 |-  ( y = ( 2nd ` z ) -> <. 2 , y >. = <. 2 , ( 2nd ` z ) >. )
14 13 preq2d 
 |-  ( y = ( 2nd ` z ) -> { <. 1 , ( 1st ` z ) >. , <. 2 , y >. } = { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } )
15 prex 
 |-  { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } e. _V
16 12 14 2 15 ovmpo 
 |-  ( ( ( 1st ` z ) e. RR /\ ( 2nd ` z ) e. RR ) -> ( ( 1st ` z ) F ( 2nd ` z ) ) = { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } )
17 9 10 16 syl2anc 
 |-  ( z e. ( RR X. RR ) -> ( ( 1st ` z ) F ( 2nd ` z ) ) = { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } )
18 8 17 eqtrd 
 |-  ( z e. ( RR X. RR ) -> ( F ` z ) = { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } )
19 eqid 
 |-  { 1 , 2 } = { 1 , 2 }
20 19 1 prelrrx2 
 |-  ( ( ( 1st ` z ) e. RR /\ ( 2nd ` z ) e. RR ) -> { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } e. R )
21 9 10 20 syl2anc 
 |-  ( z e. ( RR X. RR ) -> { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } e. R )
22 18 21 eqeltrd 
 |-  ( z e. ( RR X. RR ) -> ( F ` z ) e. R )
23 22 rgen 
 |-  A. z e. ( RR X. RR ) ( F ` z ) e. R
24 ffnfv 
 |-  ( F : ( RR X. RR ) --> R <-> ( F Fn ( RR X. RR ) /\ A. z e. ( RR X. RR ) ( F ` z ) e. R ) )
25 4 23 24 mpbir2an 
 |-  F : ( RR X. RR ) --> R
26 opex 
 |-  <. 1 , ( 1st ` z ) >. e. _V
27 opex 
 |-  <. 2 , ( 2nd ` z ) >. e. _V
28 opex 
 |-  <. 1 , ( 1st ` w ) >. e. _V
29 opex 
 |-  <. 2 , ( 2nd ` w ) >. e. _V
30 26 27 28 29 preq12b 
 |-  ( { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } = { <. 1 , ( 1st ` w ) >. , <. 2 , ( 2nd ` w ) >. } <-> ( ( <. 1 , ( 1st ` z ) >. = <. 1 , ( 1st ` w ) >. /\ <. 2 , ( 2nd ` z ) >. = <. 2 , ( 2nd ` w ) >. ) \/ ( <. 1 , ( 1st ` z ) >. = <. 2 , ( 2nd ` w ) >. /\ <. 2 , ( 2nd ` z ) >. = <. 1 , ( 1st ` w ) >. ) ) )
31 1ex 
 |-  1 e. _V
32 fvex 
 |-  ( 1st ` z ) e. _V
33 31 32 opth 
 |-  ( <. 1 , ( 1st ` z ) >. = <. 1 , ( 1st ` w ) >. <-> ( 1 = 1 /\ ( 1st ` z ) = ( 1st ` w ) ) )
34 33 simprbi 
 |-  ( <. 1 , ( 1st ` z ) >. = <. 1 , ( 1st ` w ) >. -> ( 1st ` z ) = ( 1st ` w ) )
35 2ex 
 |-  2 e. _V
36 fvex 
 |-  ( 2nd ` z ) e. _V
37 35 36 opth 
 |-  ( <. 2 , ( 2nd ` z ) >. = <. 2 , ( 2nd ` w ) >. <-> ( 2 = 2 /\ ( 2nd ` z ) = ( 2nd ` w ) ) )
38 37 simprbi 
 |-  ( <. 2 , ( 2nd ` z ) >. = <. 2 , ( 2nd ` w ) >. -> ( 2nd ` z ) = ( 2nd ` w ) )
39 34 38 anim12i 
 |-  ( ( <. 1 , ( 1st ` z ) >. = <. 1 , ( 1st ` w ) >. /\ <. 2 , ( 2nd ` z ) >. = <. 2 , ( 2nd ` w ) >. ) -> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) )
40 39 a1d 
 |-  ( ( <. 1 , ( 1st ` z ) >. = <. 1 , ( 1st ` w ) >. /\ <. 2 , ( 2nd ` z ) >. = <. 2 , ( 2nd ` w ) >. ) -> ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) ) )
41 31 32 opth 
 |-  ( <. 1 , ( 1st ` z ) >. = <. 2 , ( 2nd ` w ) >. <-> ( 1 = 2 /\ ( 1st ` z ) = ( 2nd ` w ) ) )
42 35 36 opth 
 |-  ( <. 2 , ( 2nd ` z ) >. = <. 1 , ( 1st ` w ) >. <-> ( 2 = 1 /\ ( 2nd ` z ) = ( 1st ` w ) ) )
43 1ne2 
 |-  1 =/= 2
44 eqneqall 
 |-  ( 1 = 2 -> ( 1 =/= 2 -> ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) ) ) )
45 43 44 mpi 
 |-  ( 1 = 2 -> ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) ) )
46 45 ad2antrr 
 |-  ( ( ( 1 = 2 /\ ( 1st ` z ) = ( 2nd ` w ) ) /\ ( 2 = 1 /\ ( 2nd ` z ) = ( 1st ` w ) ) ) -> ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) ) )
47 41 42 46 syl2anb 
 |-  ( ( <. 1 , ( 1st ` z ) >. = <. 2 , ( 2nd ` w ) >. /\ <. 2 , ( 2nd ` z ) >. = <. 1 , ( 1st ` w ) >. ) -> ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) ) )
48 40 47 jaoi 
 |-  ( ( ( <. 1 , ( 1st ` z ) >. = <. 1 , ( 1st ` w ) >. /\ <. 2 , ( 2nd ` z ) >. = <. 2 , ( 2nd ` w ) >. ) \/ ( <. 1 , ( 1st ` z ) >. = <. 2 , ( 2nd ` w ) >. /\ <. 2 , ( 2nd ` z ) >. = <. 1 , ( 1st ` w ) >. ) ) -> ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) ) )
49 30 48 sylbi 
 |-  ( { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } = { <. 1 , ( 1st ` w ) >. , <. 2 , ( 2nd ` w ) >. } -> ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) ) )
50 49 com12 
 |-  ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } = { <. 1 , ( 1st ` w ) >. , <. 2 , ( 2nd ` w ) >. } -> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) ) )
51 1st2nd2 
 |-  ( w e. ( RR X. RR ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
52 51 fveq2d 
 |-  ( w e. ( RR X. RR ) -> ( F ` w ) = ( F ` <. ( 1st ` w ) , ( 2nd ` w ) >. ) )
53 df-ov 
 |-  ( ( 1st ` w ) F ( 2nd ` w ) ) = ( F ` <. ( 1st ` w ) , ( 2nd ` w ) >. )
54 52 53 eqtr4di 
 |-  ( w e. ( RR X. RR ) -> ( F ` w ) = ( ( 1st ` w ) F ( 2nd ` w ) ) )
55 xp1st 
 |-  ( w e. ( RR X. RR ) -> ( 1st ` w ) e. RR )
56 xp2nd 
 |-  ( w e. ( RR X. RR ) -> ( 2nd ` w ) e. RR )
57 opeq2 
 |-  ( x = ( 1st ` w ) -> <. 1 , x >. = <. 1 , ( 1st ` w ) >. )
58 57 preq1d 
 |-  ( x = ( 1st ` w ) -> { <. 1 , x >. , <. 2 , y >. } = { <. 1 , ( 1st ` w ) >. , <. 2 , y >. } )
59 opeq2 
 |-  ( y = ( 2nd ` w ) -> <. 2 , y >. = <. 2 , ( 2nd ` w ) >. )
60 59 preq2d 
 |-  ( y = ( 2nd ` w ) -> { <. 1 , ( 1st ` w ) >. , <. 2 , y >. } = { <. 1 , ( 1st ` w ) >. , <. 2 , ( 2nd ` w ) >. } )
61 prex 
 |-  { <. 1 , ( 1st ` w ) >. , <. 2 , ( 2nd ` w ) >. } e. _V
62 58 60 2 61 ovmpo 
 |-  ( ( ( 1st ` w ) e. RR /\ ( 2nd ` w ) e. RR ) -> ( ( 1st ` w ) F ( 2nd ` w ) ) = { <. 1 , ( 1st ` w ) >. , <. 2 , ( 2nd ` w ) >. } )
63 55 56 62 syl2anc 
 |-  ( w e. ( RR X. RR ) -> ( ( 1st ` w ) F ( 2nd ` w ) ) = { <. 1 , ( 1st ` w ) >. , <. 2 , ( 2nd ` w ) >. } )
64 54 63 eqtrd 
 |-  ( w e. ( RR X. RR ) -> ( F ` w ) = { <. 1 , ( 1st ` w ) >. , <. 2 , ( 2nd ` w ) >. } )
65 18 64 eqeqan12d 
 |-  ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( ( F ` z ) = ( F ` w ) <-> { <. 1 , ( 1st ` z ) >. , <. 2 , ( 2nd ` z ) >. } = { <. 1 , ( 1st ` w ) >. , <. 2 , ( 2nd ` w ) >. } ) )
66 5 51 eqeqan12d 
 |-  ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( z = w <-> <. ( 1st ` z ) , ( 2nd ` z ) >. = <. ( 1st ` w ) , ( 2nd ` w ) >. ) )
67 32 36 opth 
 |-  ( <. ( 1st ` z ) , ( 2nd ` z ) >. = <. ( 1st ` w ) , ( 2nd ` w ) >. <-> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) )
68 66 67 bitrdi 
 |-  ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( z = w <-> ( ( 1st ` z ) = ( 1st ` w ) /\ ( 2nd ` z ) = ( 2nd ` w ) ) ) )
69 50 65 68 3imtr4d 
 |-  ( ( z e. ( RR X. RR ) /\ w e. ( RR X. RR ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
70 69 rgen2 
 |-  A. z e. ( RR X. RR ) A. w e. ( RR X. RR ) ( ( F ` z ) = ( F ` w ) -> z = w )
71 dff13 
 |-  ( F : ( RR X. RR ) -1-1-> R <-> ( F : ( RR X. RR ) --> R /\ A. z e. ( RR X. RR ) A. w e. ( RR X. RR ) ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
72 25 70 71 mpbir2an 
 |-  F : ( RR X. RR ) -1-1-> R
73 1 eleq2i 
 |-  ( w e. R <-> w e. ( RR ^m { 1 , 2 } ) )
74 reex 
 |-  RR e. _V
75 prex 
 |-  { 1 , 2 } e. _V
76 74 75 elmap 
 |-  ( w e. ( RR ^m { 1 , 2 } ) <-> w : { 1 , 2 } --> RR )
77 1re 
 |-  1 e. RR
78 2re 
 |-  2 e. RR
79 fpr2g 
 |-  ( ( 1 e. RR /\ 2 e. RR ) -> ( w : { 1 , 2 } --> RR <-> ( ( w ` 1 ) e. RR /\ ( w ` 2 ) e. RR /\ w = { <. 1 , ( w ` 1 ) >. , <. 2 , ( w ` 2 ) >. } ) ) )
80 77 78 79 mp2an 
 |-  ( w : { 1 , 2 } --> RR <-> ( ( w ` 1 ) e. RR /\ ( w ` 2 ) e. RR /\ w = { <. 1 , ( w ` 1 ) >. , <. 2 , ( w ` 2 ) >. } ) )
81 73 76 80 3bitri 
 |-  ( w e. R <-> ( ( w ` 1 ) e. RR /\ ( w ` 2 ) e. RR /\ w = { <. 1 , ( w ` 1 ) >. , <. 2 , ( w ` 2 ) >. } ) )
82 opeq2 
 |-  ( u = ( w ` 1 ) -> <. 1 , u >. = <. 1 , ( w ` 1 ) >. )
83 82 preq1d 
 |-  ( u = ( w ` 1 ) -> { <. 1 , u >. , <. 2 , v >. } = { <. 1 , ( w ` 1 ) >. , <. 2 , v >. } )
84 83 eqeq2d 
 |-  ( u = ( w ` 1 ) -> ( w = { <. 1 , u >. , <. 2 , v >. } <-> w = { <. 1 , ( w ` 1 ) >. , <. 2 , v >. } ) )
85 opeq2 
 |-  ( v = ( w ` 2 ) -> <. 2 , v >. = <. 2 , ( w ` 2 ) >. )
86 85 preq2d 
 |-  ( v = ( w ` 2 ) -> { <. 1 , ( w ` 1 ) >. , <. 2 , v >. } = { <. 1 , ( w ` 1 ) >. , <. 2 , ( w ` 2 ) >. } )
87 86 eqeq2d 
 |-  ( v = ( w ` 2 ) -> ( w = { <. 1 , ( w ` 1 ) >. , <. 2 , v >. } <-> w = { <. 1 , ( w ` 1 ) >. , <. 2 , ( w ` 2 ) >. } ) )
88 84 87 rspc2ev 
 |-  ( ( ( w ` 1 ) e. RR /\ ( w ` 2 ) e. RR /\ w = { <. 1 , ( w ` 1 ) >. , <. 2 , ( w ` 2 ) >. } ) -> E. u e. RR E. v e. RR w = { <. 1 , u >. , <. 2 , v >. } )
89 81 88 sylbi 
 |-  ( w e. R -> E. u e. RR E. v e. RR w = { <. 1 , u >. , <. 2 , v >. } )
90 opeq2 
 |-  ( x = u -> <. 1 , x >. = <. 1 , u >. )
91 90 preq1d 
 |-  ( x = u -> { <. 1 , x >. , <. 2 , y >. } = { <. 1 , u >. , <. 2 , y >. } )
92 opeq2 
 |-  ( y = v -> <. 2 , y >. = <. 2 , v >. )
93 92 preq2d 
 |-  ( y = v -> { <. 1 , u >. , <. 2 , y >. } = { <. 1 , u >. , <. 2 , v >. } )
94 prex 
 |-  { <. 1 , u >. , <. 2 , v >. } e. _V
95 91 93 2 94 ovmpo 
 |-  ( ( u e. RR /\ v e. RR ) -> ( u F v ) = { <. 1 , u >. , <. 2 , v >. } )
96 95 eqeq2d 
 |-  ( ( u e. RR /\ v e. RR ) -> ( w = ( u F v ) <-> w = { <. 1 , u >. , <. 2 , v >. } ) )
97 96 2rexbiia 
 |-  ( E. u e. RR E. v e. RR w = ( u F v ) <-> E. u e. RR E. v e. RR w = { <. 1 , u >. , <. 2 , v >. } )
98 89 97 sylibr 
 |-  ( w e. R -> E. u e. RR E. v e. RR w = ( u F v ) )
99 fveq2 
 |-  ( z = <. u , v >. -> ( F ` z ) = ( F ` <. u , v >. ) )
100 df-ov 
 |-  ( u F v ) = ( F ` <. u , v >. )
101 99 100 eqtr4di 
 |-  ( z = <. u , v >. -> ( F ` z ) = ( u F v ) )
102 101 eqeq2d 
 |-  ( z = <. u , v >. -> ( w = ( F ` z ) <-> w = ( u F v ) ) )
103 102 rexxp 
 |-  ( E. z e. ( RR X. RR ) w = ( F ` z ) <-> E. u e. RR E. v e. RR w = ( u F v ) )
104 98 103 sylibr 
 |-  ( w e. R -> E. z e. ( RR X. RR ) w = ( F ` z ) )
105 104 rgen 
 |-  A. w e. R E. z e. ( RR X. RR ) w = ( F ` z )
106 dffo3 
 |-  ( F : ( RR X. RR ) -onto-> R <-> ( F : ( RR X. RR ) --> R /\ A. w e. R E. z e. ( RR X. RR ) w = ( F ` z ) ) )
107 25 105 106 mpbir2an 
 |-  F : ( RR X. RR ) -onto-> R
108 df-f1o 
 |-  ( F : ( RR X. RR ) -1-1-onto-> R <-> ( F : ( RR X. RR ) -1-1-> R /\ F : ( RR X. RR ) -onto-> R ) )
109 72 107 108 mpbir2an 
 |-  F : ( RR X. RR ) -1-1-onto-> R