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 |
|
df-br |
|- ( X O Y <-> <. X , Y >. e. O ) |
3 |
1
|
eleq2i |
|- ( <. X , Y >. e. O <-> <. X , Y >. e. { <. x , y >. | ( ( x e. R /\ y e. R ) /\ ( ( x ` 1 ) < ( y ` 1 ) \/ ( ( x ` 1 ) = ( y ` 1 ) /\ ( x ` 2 ) < ( y ` 2 ) ) ) ) } ) |
4 |
2 3
|
bitri |
|- ( X O Y <-> <. X , Y >. e. { <. x , y >. | ( ( x e. R /\ y e. R ) /\ ( ( x ` 1 ) < ( y ` 1 ) \/ ( ( x ` 1 ) = ( y ` 1 ) /\ ( x ` 2 ) < ( y ` 2 ) ) ) ) } ) |
5 |
|
fveq1 |
|- ( x = X -> ( x ` 1 ) = ( X ` 1 ) ) |
6 |
|
fveq1 |
|- ( y = Y -> ( y ` 1 ) = ( Y ` 1 ) ) |
7 |
5 6
|
breqan12d |
|- ( ( x = X /\ y = Y ) -> ( ( x ` 1 ) < ( y ` 1 ) <-> ( X ` 1 ) < ( Y ` 1 ) ) ) |
8 |
5 6
|
eqeqan12d |
|- ( ( x = X /\ y = Y ) -> ( ( x ` 1 ) = ( y ` 1 ) <-> ( X ` 1 ) = ( Y ` 1 ) ) ) |
9 |
|
fveq1 |
|- ( x = X -> ( x ` 2 ) = ( X ` 2 ) ) |
10 |
|
fveq1 |
|- ( y = Y -> ( y ` 2 ) = ( Y ` 2 ) ) |
11 |
9 10
|
breqan12d |
|- ( ( x = X /\ y = Y ) -> ( ( x ` 2 ) < ( y ` 2 ) <-> ( X ` 2 ) < ( Y ` 2 ) ) ) |
12 |
8 11
|
anbi12d |
|- ( ( x = X /\ y = Y ) -> ( ( ( x ` 1 ) = ( y ` 1 ) /\ ( x ` 2 ) < ( y ` 2 ) ) <-> ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) |
13 |
7 12
|
orbi12d |
|- ( ( x = X /\ y = Y ) -> ( ( ( x ` 1 ) < ( y ` 1 ) \/ ( ( x ` 1 ) = ( y ` 1 ) /\ ( x ` 2 ) < ( y ` 2 ) ) ) <-> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) ) |
14 |
13
|
opelopab2a |
|- ( ( X e. R /\ Y e. R ) -> ( <. X , Y >. e. { <. x , y >. | ( ( x e. R /\ y e. R ) /\ ( ( x ` 1 ) < ( y ` 1 ) \/ ( ( x ` 1 ) = ( y ` 1 ) /\ ( x ` 2 ) < ( y ` 2 ) ) ) ) } <-> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) ) |
15 |
4 14
|
syl5bb |
|- ( ( X e. R /\ Y e. R ) -> ( X O Y <-> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) ) |