Metamath Proof Explorer

Theorem rrx2plord2

Description: The lexicographical ordering for points in the two dimensional Euclidean plane: if the first coordinates of two points are equal, a point is less than another point iff the second coordinate of the point is less than the second coordinate of the other point. (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 } )
Assertion rrx2plord2 
|- ( ( X e. R /\ Y e. R /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X O Y <-> ( 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 rrx2plord2.r 
 |-  R = ( RR ^m { 1 , 2 } )
3 1 rrx2plord 
 |-  ( ( X e. R /\ Y e. R ) -> ( X O Y <-> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) )
4 3 3adant3 
 |-  ( ( X e. R /\ Y e. R /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X O Y <-> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) )
5 eqid 
 |-  { 1 , 2 } = { 1 , 2 }
6 5 2 rrx2pxel 
 |-  ( X e. R -> ( X ` 1 ) e. RR )
7 6 adantr 
 |-  ( ( X e. R /\ Y e. R ) -> ( X ` 1 ) e. RR )
8 ltne 
 |-  ( ( ( X ` 1 ) e. RR /\ ( X ` 1 ) < ( Y ` 1 ) ) -> ( Y ` 1 ) =/= ( X ` 1 ) )
9 8 necomd 
 |-  ( ( ( X ` 1 ) e. RR /\ ( X ` 1 ) < ( Y ` 1 ) ) -> ( X ` 1 ) =/= ( Y ` 1 ) )
10 7 9 sylan 
 |-  ( ( ( X e. R /\ Y e. R ) /\ ( X ` 1 ) < ( Y ` 1 ) ) -> ( X ` 1 ) =/= ( Y ` 1 ) )
11 10 ex 
 |-  ( ( X e. R /\ Y e. R ) -> ( ( X ` 1 ) < ( Y ` 1 ) -> ( X ` 1 ) =/= ( Y ` 1 ) ) )
12 eqneqall 
 |-  ( ( X ` 1 ) = ( Y ` 1 ) -> ( ( X ` 1 ) =/= ( Y ` 1 ) -> ( X ` 2 ) < ( Y ` 2 ) ) )
13 11 12 syl9 
 |-  ( ( X e. R /\ Y e. R ) -> ( ( X ` 1 ) = ( Y ` 1 ) -> ( ( X ` 1 ) < ( Y ` 1 ) -> ( X ` 2 ) < ( Y ` 2 ) ) ) )
14 13 3impia 
 |-  ( ( X e. R /\ Y e. R /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( X ` 1 ) < ( Y ` 1 ) -> ( X ` 2 ) < ( Y ` 2 ) ) )
15 14 com12 
 |-  ( ( X ` 1 ) < ( Y ` 1 ) -> ( ( X e. R /\ Y e. R /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X ` 2 ) < ( Y ` 2 ) ) )
16 simpr 
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) -> ( X ` 2 ) < ( Y ` 2 ) )
17 16 a1d 
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) -> ( ( X e. R /\ Y e. R /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X ` 2 ) < ( Y ` 2 ) ) )
18 15 17 jaoi 
 |-  ( ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) -> ( ( X e. R /\ Y e. R /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X ` 2 ) < ( Y ` 2 ) ) )
19 18 com12 
 |-  ( ( X e. R /\ Y e. R /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) -> ( X ` 2 ) < ( Y ` 2 ) ) )
20 olc 
 |-  ( ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) -> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) )
21 20 ex 
 |-  ( ( X ` 1 ) = ( Y ` 1 ) -> ( ( X ` 2 ) < ( Y ` 2 ) -> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) )
22 21 3ad2ant3 
 |-  ( ( X e. R /\ Y e. R /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( X ` 2 ) < ( Y ` 2 ) -> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) )
23 19 22 impbid 
 |-  ( ( X e. R /\ Y e. R /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) <-> ( X ` 2 ) < ( Y ` 2 ) ) )
24 4 23 bitrd 
 |-  ( ( X e. R /\ Y e. R /\ ( X ` 1 ) = ( Y ` 1 ) ) -> ( X O Y <-> ( X ` 2 ) < ( Y ` 2 ) ) )