Metamath Proof Explorer

Theorem rrx2plordisom

Description: The set of points in the two dimensional Euclidean plane with the lexicographical ordering is isomorphic to the cartesian product of the real numbers with the lexicographical ordering implied by the ordering of the real numbers. (Contributed by AV, 12-Mar-2023)

Ref Expression
Hypotheses rrx2plord.o 
|- O = { <. x , y >. | ( ( x e. R /\ y e. R ) /\ ( ( x ` 0 ) < ( y ` 0 ) \/ ( ( x ` 0 ) = ( y ` 0 ) /\ ( x ` 1 ) < ( y ` 1 ) ) ) ) }
rrx2plord2.r 
|- R = ( RR ^m ( 0 ..^ 2 ) )
rrx2plordisom.f 
|- F = ( x e. RR , y e. RR |-> <" x y "> )
rrx2plordisom.t 
|- T = { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) }
Assertion rrx2plordisom 
|- F Isom T , O ( ( RR X. RR ) , R )

Proof

Step Hyp Ref Expression
1 rrx2plord.o 
 |-  O = { <. x , y >. | ( ( x e. R /\ y e. R ) /\ ( ( x ` 0 ) < ( y ` 0 ) \/ ( ( x ` 0 ) = ( y ` 0 ) /\ ( x ` 1 ) < ( y ` 1 ) ) ) ) }
2 rrx2plord2.r 
 |-  R = ( RR ^m ( 0 ..^ 2 ) )
3 rrx2plordisom.f 
 |-  F = ( x e. RR , y e. RR |-> <" x y "> )
4 rrx2plordisom.t 
 |-  T = { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) }
5 eqid 
 |-  ( x e. RR , y e. RR |-> <" x y "> ) = ( x e. RR , y e. RR |-> <" x y "> )
6 2 5 rrx2xpref1o 
 |-  ( x e. RR , y e. RR |-> <" x y "> ) : ( RR X. RR ) -1-1-onto-> R
7 elxpi 
 |-  ( a e. ( RR X. RR ) -> E. c E. d ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) )
8 elxpi 
 |-  ( b e. ( RR X. RR ) -> E. e E. f ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) )
9 df-br 
 |-  ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> <. a , b >. e. { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } )
10 opelxpi 
 |-  ( ( c e. RR /\ d e. RR ) -> <. c , d >. e. ( RR X. RR ) )
11 10 adantl 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> <. c , d >. e. ( RR X. RR ) )
12 eleq1 
 |-  ( a = <. c , d >. -> ( a e. ( RR X. RR ) <-> <. c , d >. e. ( RR X. RR ) ) )
13 12 adantr 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( a e. ( RR X. RR ) <-> <. c , d >. e. ( RR X. RR ) ) )
14 11 13 mpbird 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> a e. ( RR X. RR ) )
15 opelxpi 
 |-  ( ( e e. RR /\ f e. RR ) -> <. e , f >. e. ( RR X. RR ) )
16 15 adantl 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> <. e , f >. e. ( RR X. RR ) )
17 eleq1 
 |-  ( b = <. e , f >. -> ( b e. ( RR X. RR ) <-> <. e , f >. e. ( RR X. RR ) ) )
18 17 adantr 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( b e. ( RR X. RR ) <-> <. e , f >. e. ( RR X. RR ) ) )
19 16 18 mpbird 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> b e. ( RR X. RR ) )
20 fveq2 
 |-  ( x = a -> ( 1st ` x ) = ( 1st ` a ) )
21 fveq2 
 |-  ( y = b -> ( 1st ` y ) = ( 1st ` b ) )
22 20 21 breqan12d 
 |-  ( ( x = a /\ y = b ) -> ( ( 1st ` x ) < ( 1st ` y ) <-> ( 1st ` a ) < ( 1st ` b ) ) )
23 20 21 eqeqan12d 
 |-  ( ( x = a /\ y = b ) -> ( ( 1st ` x ) = ( 1st ` y ) <-> ( 1st ` a ) = ( 1st ` b ) ) )
24 fveq2 
 |-  ( x = a -> ( 2nd ` x ) = ( 2nd ` a ) )
25 fveq2 
 |-  ( y = b -> ( 2nd ` y ) = ( 2nd ` b ) )
26 24 25 breqan12d 
 |-  ( ( x = a /\ y = b ) -> ( ( 2nd ` x ) < ( 2nd ` y ) <-> ( 2nd ` a ) < ( 2nd ` b ) ) )
27 23 26 anbi12d 
 |-  ( ( x = a /\ y = b ) -> ( ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) <-> ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) < ( 2nd ` b ) ) ) )
28 22 27 orbi12d 
 |-  ( ( x = a /\ y = b ) -> ( ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) <-> ( ( 1st ` a ) < ( 1st ` b ) \/ ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) < ( 2nd ` b ) ) ) ) )
29 28 opelopab2a 
 |-  ( ( a e. ( RR X. RR ) /\ b e. ( RR X. RR ) ) -> ( <. a , b >. e. { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } <-> ( ( 1st ` a ) < ( 1st ` b ) \/ ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) < ( 2nd ` b ) ) ) ) )
30 14 19 29 syl2an 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( <. a , b >. e. { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } <-> ( ( 1st ` a ) < ( 1st ` b ) \/ ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) < ( 2nd ` b ) ) ) ) )
31 9 30 bitrid 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> ( ( 1st ` a ) < ( 1st ` b ) \/ ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) < ( 2nd ` b ) ) ) ) )
32 vex 
 |-  c e. _V
33 s2fv0 
 |-  ( c e. _V -> ( <" c d "> ` 0 ) = c )
34 32 33 mp1i 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( <" c d "> ` 0 ) = c )
35 vex 
 |-  e e. _V
36 s2fv0 
 |-  ( e e. _V -> ( <" e f "> ` 0 ) = e )
37 35 36 mp1i 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( <" e f "> ` 0 ) = e )
38 34 37 breq12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( <" c d "> ` 0 ) < ( <" e f "> ` 0 ) <-> c < e ) )
39 34 37 eqeq12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( <" c d "> ` 0 ) = ( <" e f "> ` 0 ) <-> c = e ) )
40 vex 
 |-  d e. _V
41 s2fv1 
 |-  ( d e. _V -> ( <" c d "> ` 1 ) = d )
42 40 41 mp1i 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( <" c d "> ` 1 ) = d )
43 vex 
 |-  f e. _V
44 s2fv1 
 |-  ( f e. _V -> ( <" e f "> ` 1 ) = f )
45 43 44 mp1i 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( <" e f "> ` 1 ) = f )
46 42 45 breq12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( <" c d "> ` 1 ) < ( <" e f "> ` 1 ) <-> d < f ) )
47 39 46 anbi12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( ( <" c d "> ` 0 ) = ( <" e f "> ` 0 ) /\ ( <" c d "> ` 1 ) < ( <" e f "> ` 1 ) ) <-> ( c = e /\ d < f ) ) )
48 38 47 orbi12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( ( <" c d "> ` 0 ) < ( <" e f "> ` 0 ) \/ ( ( <" c d "> ` 0 ) = ( <" e f "> ` 0 ) /\ ( <" c d "> ` 1 ) < ( <" e f "> ` 1 ) ) ) <-> ( c < e \/ ( c = e /\ d < f ) ) ) )
49 eqid 
 |-  ( 0 ..^ 2 ) = ( 0 ..^ 2 )
50 49 2 prelrrx2 
 |-  ( ( c e. RR /\ d e. RR ) -> <" c d "> e. R )
51 50 adantl 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> <" c d "> e. R )
52 49 2 prelrrx2 
 |-  ( ( e e. RR /\ f e. RR ) -> <" e f "> e. R )
53 52 adantl 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> <" e f "> e. R )
54 1 rrx2plord 
 |-  ( ( <" c d "> e. R /\ <" e f "> e. R ) -> ( <" c d "> O <" e f "> <-> ( ( <" c d "> ` 0 ) < ( <" e f "> ` 0 ) \/ ( ( <" c d "> ` 0 ) = ( <" e f "> ` 0 ) /\ ( <" c d "> ` 1 ) < ( <" e f "> ` 1 ) ) ) ) )
55 51 53 54 syl2an 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( <" c d "> O <" e f "> <-> ( ( <" c d "> ` 0 ) < ( <" e f "> ` 0 ) \/ ( ( <" c d "> ` 0 ) = ( <" e f "> ` 0 ) /\ ( <" c d "> ` 1 ) < ( <" e f "> ` 1 ) ) ) ) )
56 32 40 op1std 
 |-  ( a = <. c , d >. -> ( 1st ` a ) = c )
57 56 adantr 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( 1st ` a ) = c )
58 35 43 op1std 
 |-  ( b = <. e , f >. -> ( 1st ` b ) = e )
59 58 adantr 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( 1st ` b ) = e )
60 57 59 breqan12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( 1st ` a ) < ( 1st ` b ) <-> c < e ) )
61 57 59 eqeqan12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( 1st ` a ) = ( 1st ` b ) <-> c = e ) )
62 32 40 op2ndd 
 |-  ( a = <. c , d >. -> ( 2nd ` a ) = d )
63 62 adantr 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( 2nd ` a ) = d )
64 35 43 op2ndd 
 |-  ( b = <. e , f >. -> ( 2nd ` b ) = f )
65 64 adantr 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( 2nd ` b ) = f )
66 63 65 breqan12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( 2nd ` a ) < ( 2nd ` b ) <-> d < f ) )
67 61 66 anbi12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) < ( 2nd ` b ) ) <-> ( c = e /\ d < f ) ) )
68 60 67 orbi12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( ( 1st ` a ) < ( 1st ` b ) \/ ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) < ( 2nd ` b ) ) ) <-> ( c < e \/ ( c = e /\ d < f ) ) ) )
69 48 55 68 3bitr4rd 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( ( 1st ` a ) < ( 1st ` b ) \/ ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) < ( 2nd ` b ) ) ) <-> <" c d "> O <" e f "> ) )
70 fveq2 
 |-  ( a = <. c , d >. -> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) = ( ( x e. RR , y e. RR |-> <" x y "> ) ` <. c , d >. ) )
71 df-ov 
 |-  ( c ( x e. RR , y e. RR |-> <" x y "> ) d ) = ( ( x e. RR , y e. RR |-> <" x y "> ) ` <. c , d >. )
72 70 71 eqtr4di 
 |-  ( a = <. c , d >. -> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) = ( c ( x e. RR , y e. RR |-> <" x y "> ) d ) )
73 eqidd 
 |-  ( ( c e. RR /\ d e. RR ) -> ( x e. RR , y e. RR |-> <" x y "> ) = ( x e. RR , y e. RR |-> <" x y "> ) )
74 simprl 
 |-  ( ( ( c e. RR /\ d e. RR ) /\ ( x = c /\ y = d ) ) -> x = c )
75 simprr 
 |-  ( ( ( c e. RR /\ d e. RR ) /\ ( x = c /\ y = d ) ) -> y = d )
76 74 75 s2eqd 
 |-  ( ( ( c e. RR /\ d e. RR ) /\ ( x = c /\ y = d ) ) -> <" x y "> = <" c d "> )
77 simpl 
 |-  ( ( c e. RR /\ d e. RR ) -> c e. RR )
78 simpr 
 |-  ( ( c e. RR /\ d e. RR ) -> d e. RR )
79 73 76 77 78 50 ovmpod 
 |-  ( ( c e. RR /\ d e. RR ) -> ( c ( x e. RR , y e. RR |-> <" x y "> ) d ) = <" c d "> )
80 72 79 sylan9eq 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) = <" c d "> )
81 80 eqcomd 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> <" c d "> = ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) )
82 fveq2 
 |-  ( b = <. e , f >. -> ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) = ( ( x e. RR , y e. RR |-> <" x y "> ) ` <. e , f >. ) )
83 df-ov 
 |-  ( e ( x e. RR , y e. RR |-> <" x y "> ) f ) = ( ( x e. RR , y e. RR |-> <" x y "> ) ` <. e , f >. )
84 82 83 eqtr4di 
 |-  ( b = <. e , f >. -> ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) = ( e ( x e. RR , y e. RR |-> <" x y "> ) f ) )
85 eqidd 
 |-  ( ( e e. RR /\ f e. RR ) -> ( x e. RR , y e. RR |-> <" x y "> ) = ( x e. RR , y e. RR |-> <" x y "> ) )
86 simprl 
 |-  ( ( ( e e. RR /\ f e. RR ) /\ ( x = e /\ y = f ) ) -> x = e )
87 simprr 
 |-  ( ( ( e e. RR /\ f e. RR ) /\ ( x = e /\ y = f ) ) -> y = f )
88 86 87 s2eqd 
 |-  ( ( ( e e. RR /\ f e. RR ) /\ ( x = e /\ y = f ) ) -> <" x y "> = <" e f "> )
89 simpl 
 |-  ( ( e e. RR /\ f e. RR ) -> e e. RR )
90 simpr 
 |-  ( ( e e. RR /\ f e. RR ) -> f e. RR )
91 85 88 89 90 52 ovmpod 
 |-  ( ( e e. RR /\ f e. RR ) -> ( e ( x e. RR , y e. RR |-> <" x y "> ) f ) = <" e f "> )
92 84 91 sylan9eq 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) = <" e f "> )
93 92 eqcomd 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> <" e f "> = ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) )
94 81 93 breqan12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( <" c d "> O <" e f "> <-> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) O ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) ) )
95 31 69 94 3bitrd 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) O ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) ) )
96 95 expcom 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) O ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) ) ) )
97 96 exlimivv 
 |-  ( E. e E. f ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) O ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) ) ) )
98 97 com12 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( E. e E. f ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) O ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) ) ) )
99 98 exlimivv 
 |-  ( E. c E. d ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( E. e E. f ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) O ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) ) ) )
100 99 imp 
 |-  ( ( E. c E. d ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ E. e E. f ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) O ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) ) )
101 7 8 100 syl2an 
 |-  ( ( a e. ( RR X. RR ) /\ b e. ( RR X. RR ) ) -> ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) O ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) ) )
102 101 rgen2 
 |-  A. a e. ( RR X. RR ) A. b e. ( RR X. RR ) ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) O ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) )
103 df-isom 
 |-  ( ( x e. RR , y e. RR |-> <" x y "> ) Isom { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } , O ( ( RR X. RR ) , R ) <-> ( ( x e. RR , y e. RR |-> <" x y "> ) : ( RR X. RR ) -1-1-onto-> R /\ A. a e. ( RR X. RR ) A. b e. ( RR X. RR ) ( a { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } b <-> ( ( x e. RR , y e. RR |-> <" x y "> ) ` a ) O ( ( x e. RR , y e. RR |-> <" x y "> ) ` b ) ) ) )
104 6 102 103 mpbir2an 
 |-  ( x e. RR , y e. RR |-> <" x y "> ) Isom { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } , O ( ( RR X. RR ) , R )
105 isoeq2 
 |-  ( T = { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } -> ( ( x e. RR , y e. RR |-> <" x y "> ) Isom T , O ( ( RR X. RR ) , R ) <-> ( x e. RR , y e. RR |-> <" x y "> ) Isom { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } , O ( ( RR X. RR ) , R ) ) )
106 4 105 ax-mp 
 |-  ( ( x e. RR , y e. RR |-> <" x y "> ) Isom T , O ( ( RR X. RR ) , R ) <-> ( x e. RR , y e. RR |-> <" x y "> ) Isom { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } , O ( ( RR X. RR ) , R ) )
107 104 106 mpbir 
 |-  ( x e. RR , y e. RR |-> <" x y "> ) Isom T , O ( ( RR X. RR ) , R )
108 isoeq1 
 |-  ( F = ( x e. RR , y e. RR |-> <" x y "> ) -> ( F Isom T , O ( ( RR X. RR ) , R ) <-> ( x e. RR , y e. RR |-> <" x y "> ) Isom T , O ( ( RR X. RR ) , R ) ) )
109 3 108 ax-mp 
 |-  ( F Isom T , O ( ( RR X. RR ) , R ) <-> ( x e. RR , y e. RR |-> <" x y "> ) Isom T , O ( ( RR X. RR ) , R ) )
110 107 109 mpbir 
 |-  F Isom T , O ( ( RR X. RR ) , R )