Metamath Proof Explorer

Theorem ltrelsr

Description: Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltrelsr 
|-

Proof

Step Hyp Ref Expression
1 df-ltr 
 |-  . | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )
2 opabssxp 
 |-  { <. x , y >. | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u )
3 1 2 eqsstri 
 |-