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 |
|
simp3 |
|- ( ( X e. R /\ Y e. R /\ ( X ` 1 ) < ( Y ` 1 ) ) -> ( X ` 1 ) < ( Y ` 1 ) ) |
3 |
2
|
orcd |
|- ( ( X e. R /\ Y e. R /\ ( X ` 1 ) < ( Y ` 1 ) ) -> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) |
4 |
1
|
rrx2plord |
|- ( ( X e. R /\ Y e. R ) -> ( X O Y <-> ( ( X ` 1 ) < ( Y ` 1 ) \/ ( ( X ` 1 ) = ( Y ` 1 ) /\ ( X ` 2 ) < ( Y ` 2 ) ) ) ) ) |
5 |
4
|
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 ) ) ) ) ) |
6 |
3 5
|
mpbird |
|- ( ( X e. R /\ Y e. R /\ ( X ` 1 ) < ( Y ` 1 ) ) -> X O Y ) |