Metamath Proof Explorer


Theorem rrx2plord

Description: The lexicographical ordering for points in the two dimensional Euclidean plane: a point is less than another point iff its first coordinate is less than the first coordinate of the other point, or the first coordinates of both points are equal and the second coordinate of the first point is less than the second coordinate of the other point: <. a , b >. <_ <. x , y >. iff ( a < x \/ ( a = x /\ b <_ y ) ) . (Contributed by AV, 12-Mar-2023)

Ref Expression
Hypothesis rrx2plord.o
|- O = { <. x , y >. | ( ( x e. R /\ y e. R ) /\ ( ( x ` 1 ) < ( y ` 1 ) \/ ( ( x ` 1 ) = ( y ` 1 ) /\ ( x ` 2 ) < ( y ` 2 ) ) ) ) }
Assertion rrx2plord
|- ( ( X e. R /\ Y e. R ) -> ( X O Y <-> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) )

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 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 ) ) ) ) )