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=12
Assertion rrx2xpreen R2

Proof

Step Hyp Ref Expression
1 rrx2xpreen.r R=12
2 reex V
3 2 2 mpoex x,y1x2yV
4 f1oeq1 f=x,y1x2yf:21-1 ontoRx,y1x2y:21-1 ontoR
5 eqid x,y1x2y=x,y1x2y
6 1 5 rrx2xpref1o x,y1x2y:21-1 ontoR
7 3 4 6 ceqsexv2d ff:21-1 ontoR
8 bren 2Rff:21-1 ontoR
9 7 8 mpbir 2R
10 9 ensymi R2