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 )