Metamath Proof Explorer

Theorem rrx2plordso

Description: The lexicographical ordering for points in the two dimensional Euclidean plane is a strict total ordering. (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 rrx2plordso 
|- O Or 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 ltso 
 |-  < Or RR
4 eqid 
 |-  { <. 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 , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) }
5 4 soxp 
 |-  ( ( < Or RR /\ < Or RR ) -> { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } Or ( RR X. RR ) )
6 3 3 5 mp2an 
 |-  { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } Or ( RR X. RR )
7 eqid 
 |-  ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } ) = ( x e. RR , y e. RR |-> { <. 1 , x >. , <. 2 , y >. } )
8 1 2 7 4 rrx2plordisom 
 |-  ( 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 )
9 isoso 
 |-  ( ( 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 , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } Or ( RR X. RR ) <-> O Or R ) )
10 8 9 ax-mp 
 |-  ( { <. x , y >. | ( ( x e. ( RR X. RR ) /\ y e. ( RR X. RR ) ) /\ ( ( 1st ` x ) < ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) < ( 2nd ` y ) ) ) ) } Or ( RR X. RR ) <-> O Or R )
11 6 10 mpbi 
 |-  O Or R