Metamath Proof Explorer


Theorem rrx2xpreen

Description: The set of points in the two dimensional Euclidean plane and the set of ordered pairs of real numbers (the cartesian product of the real numbers) are equinumerous. (Contributed by AV, 12-Mar-2023)

Ref Expression
Hypothesis rrx2xpreen.r
|- R = ( RR ^m { 1 , 2 } )
Assertion rrx2xpreen
|- R ~~ ( RR X. RR )

Proof

Step Hyp Ref Expression
1 rrx2xpreen.r
 |-  R = ( RR ^m { 1 , 2 } )
2 reex
 |-  RR e. _V
3 2 2 mpoex
 |-  ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) e. _V
4 f1oeq1
 |-  ( f = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) -> ( f : ( RR X. RR ) -1-1-onto-> R <-> ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) : ( RR X. RR ) -1-1-onto-> R ) )
5 eqid
 |-  ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } )
6 1 5 rrx2xpref1o
 |-  ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) : ( RR X. RR ) -1-1-onto-> R
7 3 4 6 ceqsexv2d
 |-  E. f f : ( RR X. RR ) -1-1-onto-> R
8 bren
 |-  ( ( RR X. RR ) ~~ R <-> E. f f : ( RR X. RR ) -1-1-onto-> R )
9 7 8 mpbir
 |-  ( RR X. RR ) ~~ R
10 9 ensymi
 |-  R ~~ ( RR X. RR )