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=xy|xRyRx1<y1x1=y1x2<y2
Assertion rrx2plord XRYRXOYX1<Y1X1=Y1X2<Y2

Proof

Step Hyp Ref Expression
1 rrx2plord.o O=xy|xRyRx1<y1x1=y1x2<y2
2 df-br XOYXYO
3 1 eleq2i XYOXYxy|xRyRx1<y1x1=y1x2<y2
4 2 3 bitri XOYXYxy|xRyRx1<y1x1=y1x2<y2
5 fveq1 x=Xx1=X1
6 fveq1 y=Yy1=Y1
7 5 6 breqan12d x=Xy=Yx1<y1X1<Y1
8 5 6 eqeqan12d x=Xy=Yx1=y1X1=Y1
9 fveq1 x=Xx2=X2
10 fveq1 y=Yy2=Y2
11 9 10 breqan12d x=Xy=Yx2<y2X2<Y2
12 8 11 anbi12d x=Xy=Yx1=y1x2<y2X1=Y1X2<Y2
13 7 12 orbi12d x=Xy=Yx1<y1x1=y1x2<y2X1<Y1X1=Y1X2<Y2
14 13 opelopab2a XRYRXYxy|xRyRx1<y1x1=y1x2<y2X1<Y1X1=Y1X2<Y2
15 4 14 syl5bb XRYRXOYX1<Y1X1=Y1X2<Y2