Theorem ltrelsr 7345

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

Assertion

Ref	Expression
ltrelsr	|- <R C_ ( R. X. R. )

Proof of Theorem ltrelsr

Dummy variables x y z w v u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ltr 7337	. 2 |- <R = { <. 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 ) <P ( w +P. v ) ) ) }
2		opabssxp 4525	. 2 |- { <. 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 ) <P ( w +P. v ) ) ) } C_ ( R. X. R. )
3	1, 2	eqsstri 3057	1 |- <R C_ ( R. X. R. )

Syntax hints:   /\ wa 103   = wceq 1290   E.wex 1427   e. wcel 1439   C_ wss 3000   <.cop 3453   class class class wbr 3851   {copab 3904   X. cxp 4450  (class class class)co 5666   [cec 6304   +P. cpp 6913   <P cltp 6915   ~R cer 6916   R.cnr 6917   <R cltr 6923

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-in 3006  df-ss 3013  df-opab 3906  df-xp 4458  df-ltr 7337

This theorem is referenced by:  gt0srpr  7355  recexgt0sr  7380  addgt0sr  7382  mulgt0sr  7384  caucvgsrlemcl  7395  caucvgsrlemasr  7396  caucvgsrlemfv  7397  ltresr  7437  axpre-ltirr  7478  axpre-lttrn  7480