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 ` 1 ) < ( y ` 1 ) \/ ( ( x ` 1 ) = ( y ` 1 ) /\ ( x ` 2 ) < ( y ` 2 ) ) ) ) }
rrx2plord2.r 
|- R = ( RR ^m { 1 , 2 } )
rrx2plordisom.f 
|- F = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , 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 ` 1 ) < ( y ` 1 ) \/ ( ( x ` 1 ) = ( y ` 1 ) /\ ( x ` 2 ) < ( y ` 2 ) ) ) ) }
2 rrx2plord2.r 
 |-  R = ( RR ^m { 1 , 2 } )
3 rrx2plordisom.f 
 |-  F = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , 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 |-> { <. 1 , x >. , <. 2 , y >. } ) = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } )
6 2 5 rrx2xpref1o 
 |-  ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , 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 1ne2 
 |-  1 =/= 2
33 1ex 
 |-  1 e. _V
34 vex 
 |-  c e. _V
35 33 34 fvpr1 
 |-  ( 1 =/= 2 -> ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) = c )
36 32 35 mp1i 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) = c )
37 vex 
 |-  e e. _V
38 33 37 fvpr1 
 |-  ( 1 =/= 2 -> ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) = e )
39 32 38 mp1i 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) = e )
40 36 39 breq12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) < ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) <-> c < e ) )
41 36 39 eqeq12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) = ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) <-> c = e ) )
42 2ex 
 |-  2 e. _V
43 vex 
 |-  d e. _V
44 42 43 fvpr2 
 |-  ( 1 =/= 2 -> ( { <. 1 , c >. , <. 2 , d >. } ` 2 ) = d )
45 32 44 mp1i 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( { <. 1 , c >. , <. 2 , d >. } ` 2 ) = d )
46 vex 
 |-  f e. _V
47 42 46 fvpr2 
 |-  ( 1 =/= 2 -> ( { <. 1 , e >. , <. 2 , f >. } ` 2 ) = f )
48 32 47 mp1i 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( { <. 1 , e >. , <. 2 , f >. } ` 2 ) = f )
49 45 48 breq12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( { <. 1 , c >. , <. 2 , d >. } ` 2 ) < ( { <. 1 , e >. , <. 2 , f >. } ` 2 ) <-> d < f ) )
50 41 49 anbi12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) = ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) /\ ( { <. 1 , c >. , <. 2 , d >. } ` 2 ) < ( { <. 1 , e >. , <. 2 , f >. } ` 2 ) ) <-> ( c = e /\ d < f ) ) )
51 40 50 orbi12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( ( ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) < ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) \/ ( ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) = ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) /\ ( { <. 1 , c >. , <. 2 , d >. } ` 2 ) < ( { <. 1 , e >. , <. 2 , f >. } ` 2 ) ) ) <-> ( c < e \/ ( c = e /\ d < f ) ) ) )
52 eqid 
 |-  { 1 , 2 } = { 1 , 2 }
53 52 2 prelrrx2 
 |-  ( ( c e. RR /\ d e. RR ) -> { <. 1 , c >. , <. 2 , d >. } e. R )
54 53 adantl 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> { <. 1 , c >. , <. 2 , d >. } e. R )
55 52 2 prelrrx2 
 |-  ( ( e e. RR /\ f e. RR ) -> { <. 1 , e >. , <. 2 , f >. } e. R )
56 55 adantl 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> { <. 1 , e >. , <. 2 , f >. } e. R )
57 1 rrx2plord 
 |-  ( ( { <. 1 , c >. , <. 2 , d >. } e. R /\ { <. 1 , e >. , <. 2 , f >. } e. R ) -> ( { <. 1 , c >. , <. 2 , d >. } O { <. 1 , e >. , <. 2 , f >. } <-> ( ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) < ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) \/ ( ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) = ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) /\ ( { <. 1 , c >. , <. 2 , d >. } ` 2 ) < ( { <. 1 , e >. , <. 2 , f >. } ` 2 ) ) ) ) )
58 54 56 57 syl2an 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( { <. 1 , c >. , <. 2 , d >. } O { <. 1 , e >. , <. 2 , f >. } <-> ( ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) < ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) \/ ( ( { <. 1 , c >. , <. 2 , d >. } ` 1 ) = ( { <. 1 , e >. , <. 2 , f >. } ` 1 ) /\ ( { <. 1 , c >. , <. 2 , d >. } ` 2 ) < ( { <. 1 , e >. , <. 2 , f >. } ` 2 ) ) ) ) )
59 34 43 op1std 
 |-  ( a = <. c , d >. -> ( 1st ` a ) = c )
60 59 adantr 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( 1st ` a ) = c )
61 37 46 op1std 
 |-  ( b = <. e , f >. -> ( 1st ` b ) = e )
62 61 adantr 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( 1st ` b ) = e )
63 60 62 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 ) )
64 60 62 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 ) )
65 34 43 op2ndd 
 |-  ( a = <. c , d >. -> ( 2nd ` a ) = d )
66 65 adantr 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( 2nd ` a ) = d )
67 37 46 op2ndd 
 |-  ( b = <. e , f >. -> ( 2nd ` b ) = f )
68 67 adantr 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( 2nd ` b ) = f )
69 66 68 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 ) )
70 64 69 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 ) ) )
71 63 70 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 ) ) ) )
72 51 58 71 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 ) ) ) <-> { <. 1 , c >. , <. 2 , d >. } O { <. 1 , e >. , <. 2 , f >. } ) )
73 fveq2 
 |-  ( a = <. c , d >. -> ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) = ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` <. c , d >. ) )
74 df-ov 
 |-  ( c ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) d ) = ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` <. c , d >. )
75 73 74 eqtr4di 
 |-  ( a = <. c , d >. -> ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) = ( c ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) d ) )
76 eqidd 
 |-  ( ( c e. RR /\ d e. RR ) -> ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) )
77 opeq2 
 |-  ( x = c -> <. 1 , x >. = <. 1 , c >. )
78 77 adantr 
 |-  ( ( x = c /\ y = d ) -> <. 1 , x >. = <. 1 , c >. )
79 opeq2 
 |-  ( y = d -> <. 2 , y >. = <. 2 , d >. )
80 79 adantl 
 |-  ( ( x = c /\ y = d ) -> <. 2 , y >. = <. 2 , d >. )
81 78 80 preq12d 
 |-  ( ( x = c /\ y = d ) -> { <. 1 , x >. , <. 2 , y >. } = { <. 1 , c >. , <. 2 , d >. } )
82 81 adantl 
 |-  ( ( ( c e. RR /\ d e. RR ) /\ ( x = c /\ y = d ) ) -> { <. 1 , x >. , <. 2 , y >. } = { <. 1 , c >. , <. 2 , d >. } )
83 simpl 
 |-  ( ( c e. RR /\ d e. RR ) -> c e. RR )
84 simpr 
 |-  ( ( c e. RR /\ d e. RR ) -> d e. RR )
85 prex 
 |-  { <. 1 , c >. , <. 2 , d >. } e. _V
86 85 a1i 
 |-  ( ( c e. RR /\ d e. RR ) -> { <. 1 , c >. , <. 2 , d >. } e. _V )
87 76 82 83 84 86 ovmpod 
 |-  ( ( c e. RR /\ d e. RR ) -> ( c ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) d ) = { <. 1 , c >. , <. 2 , d >. } )
88 75 87 sylan9eq 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) = { <. 1 , c >. , <. 2 , d >. } )
89 88 eqcomd 
 |-  ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) -> { <. 1 , c >. , <. 2 , d >. } = ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) )
90 fveq2 
 |-  ( b = <. e , f >. -> ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) = ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` <. e , f >. ) )
91 df-ov 
 |-  ( e ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) f ) = ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` <. e , f >. )
92 90 91 eqtr4di 
 |-  ( b = <. e , f >. -> ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) = ( e ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) f ) )
93 eqidd 
 |-  ( ( e e. RR /\ f e. RR ) -> ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) )
94 opeq2 
 |-  ( x = e -> <. 1 , x >. = <. 1 , e >. )
95 94 adantr 
 |-  ( ( x = e /\ y = f ) -> <. 1 , x >. = <. 1 , e >. )
96 opeq2 
 |-  ( y = f -> <. 2 , y >. = <. 2 , f >. )
97 96 adantl 
 |-  ( ( x = e /\ y = f ) -> <. 2 , y >. = <. 2 , f >. )
98 95 97 preq12d 
 |-  ( ( x = e /\ y = f ) -> { <. 1 , x >. , <. 2 , y >. } = { <. 1 , e >. , <. 2 , f >. } )
99 98 adantl 
 |-  ( ( ( e e. RR /\ f e. RR ) /\ ( x = e /\ y = f ) ) -> { <. 1 , x >. , <. 2 , y >. } = { <. 1 , e >. , <. 2 , f >. } )
100 simpl 
 |-  ( ( e e. RR /\ f e. RR ) -> e e. RR )
101 simpr 
 |-  ( ( e e. RR /\ f e. RR ) -> f e. RR )
102 prex 
 |-  { <. 1 , e >. , <. 2 , f >. } e. _V
103 102 a1i 
 |-  ( ( e e. RR /\ f e. RR ) -> { <. 1 , e >. , <. 2 , f >. } e. _V )
104 93 99 100 101 103 ovmpod 
 |-  ( ( e e. RR /\ f e. RR ) -> ( e ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) f ) = { <. 1 , e >. , <. 2 , f >. } )
105 92 104 sylan9eq 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) = { <. 1 , e >. , <. 2 , f >. } )
106 105 eqcomd 
 |-  ( ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) -> { <. 1 , e >. , <. 2 , f >. } = ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) )
107 89 106 breqan12d 
 |-  ( ( ( a = <. c , d >. /\ ( c e. RR /\ d e. RR ) ) /\ ( b = <. e , f >. /\ ( e e. RR /\ f e. RR ) ) ) -> ( { <. 1 , c >. , <. 2 , d >. } O { <. 1 , e >. , <. 2 , f >. } <-> ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) O ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) ) )
108 31 72 107 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 |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) O ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) ) )
109 108 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 |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) O ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) ) ) )
110 109 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 |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) O ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) ) ) )
111 110 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 |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) O ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) ) ) )
112 111 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 |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) O ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) ) ) )
113 112 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 |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) O ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) ) )
114 7 8 113 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 |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) O ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) ) )
115 114 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 |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) O ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) )
116 df-isom 
 |-  ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , 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 |-> { <. 1 , x >. , <. 2 , 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 |-> { <. 1 , x >. , <. 2 , y >. } ) ` a ) O ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) ` b ) ) ) )
117 6 115 116 mpbir2an 
 |-  ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , 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 )
118 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 |-> { <. 1 , x >. , <. 2 , y >. } ) Isom T , O ( ( RR X. RR ) , R ) <-> ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , 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 ) ) )
119 4 118 ax-mp 
 |-  ( ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) Isom T , O ( ( RR X. RR ) , R ) <-> ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , 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 ) )
120 117 119 mpbir 
 |-  ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) Isom T , O ( ( RR X. RR ) , R )
121 isoeq1 
 |-  ( F = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) -> ( F Isom T , O ( ( RR X. RR ) , R ) <-> ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) Isom T , O ( ( RR X. RR ) , R ) ) )
122 3 121 ax-mp 
 |-  ( F Isom T , O ( ( RR X. RR ) , R ) <-> ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) Isom T , O ( ( RR X. RR ) , R ) )
123 120 122 mpbir 
 |-  F Isom T , O ( ( RR X. RR ) , R )