MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrltso Structured version   Unicode version

Theorem xrltso 10736
Description: 'Less than' is a strict ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
Assertion
Ref Expression
xrltso  |-  <  Or  RR*

Proof of Theorem xrltso
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrlttri 10734 . 2  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
x  <  y  <->  -.  (
x  =  y  \/  y  <  x ) ) )
2 xrlttr 10735 . 2  |-  ( ( x  e.  RR*  /\  y  e.  RR*  /\  z  e. 
RR* )  ->  (
( x  <  y  /\  y  <  z )  ->  x  <  z
) )
31, 2isso2i 4537 1  |-  <  Or  RR*
Colors of variables: wff set class
Syntax hints:    Or wor 4504   RR*cxr 9121    < clt 9122
This theorem is referenced by:  xrlttri2  10737  xrlttri3  10738  xrltne  10755  xmullem  10845  xmulasslem  10866  supxr  10893  supxrcl  10895  supxrun  10896  infmxrcl  10897  supxrmnf  10898  supxrunb1  10900  supxrunb2  10901  supxrub  10905  supxrlub  10906  infmxrlb  10914  infmxrgelb  10915  xrinfm0  10917  limsupval  12270  limsupgval  12272  limsupgre  12277  ramval  13378  ramcl2lem  13379  prdsdsfn  13689  prdsdsval  13702  imasdsfn  13742  imasdsval  13743  prdsmet  18402  xpsdsval  18413  prdsbl  18523  tmsxpsval2  18571  nmoval  18751  xrge0tsms2  18868  metdsval  18879  iccpnfhmeo  18972  xrhmeo  18973  ovolval  19372  ovolf  19380  ovolctb  19388  itg2val  19622  mdegval  19988  mdegldg  19991  mdegxrf  19993  mdegcl  19994  aannenlem2  20248  nmooval  22266  nmoo0  22294  nmopval  23361  nmfnval  23381  nmop0  23491  nmfn0  23492  xrsupssd  24127  xrge0iifiso  24323  esumval  24443  esumnul  24445  esum0  24446  gsumesum  24453  esumsn  24458  esumpcvgval  24470  mblfinlem2  26246  ovoliunnfl  26250  voliunnfl  26252  volsupnfl  26253  itg2addnclem  26258
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-cnex 9048  ax-resscn 9049  ax-pre-lttri 9066  ax-pre-lttrn 9067
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-po 4505  df-so 4506  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-er 6907  df-en 7112  df-dom 7113  df-sdom 7114  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127
  Copyright terms: Public domain W3C validator