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

Theorem xrltso 11117
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 11115 . 2  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
x  <  y  <->  -.  (
x  =  y  \/  y  <  x ) ) )
2 xrlttr 11116 . 2  |-  ( ( x  e.  RR*  /\  y  e.  RR*  /\  z  e. 
RR* )  ->  (
( x  <  y  /\  y  <  z )  ->  x  <  z
) )
31, 2isso2i 4672 1  |-  <  Or  RR*
Colors of variables: wff setvar class
Syntax hints:    Or wor 4639   RR*cxr 9416    < clt 9417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pow 4469  ax-pr 4530  ax-un 6371  ax-cnex 9337  ax-resscn 9338  ax-pre-lttri 9355  ax-pre-lttrn 9356
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-sbc 3186  df-csb 3288  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-pw 3861  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-opab 4350  df-mpt 4351  df-id 4635  df-po 4640  df-so 4641  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-er 7100  df-en 7310  df-dom 7311  df-sdom 7312  df-pnf 9419  df-mnf 9420  df-xr 9421  df-ltxr 9422
This theorem is referenced by:  xrlttri2  11118  xrlttri3  11119  xrltne  11136  xmullem  11226  xmulasslem  11247  supxr  11274  supxrcl  11276  supxrun  11277  infmxrcl  11278  supxrmnf  11279  supxrunb1  11281  supxrunb2  11282  supxrub  11286  supxrlub  11287  infmxrlb  11295  infmxrgelb  11296  xrinfm0  11298  limsupval  12951  limsupgval  12953  limsupgre  12958  ramval  14068  ramcl2lem  14069  prdsdsfn  14402  prdsdsval  14415  imasdsfn  14451  imasdsval  14452  prdsmet  19944  xpsdsval  19955  prdsbl  20065  tmsxpsval2  20113  nmoval  20293  xrge0tsms2  20411  metdsval  20422  iccpnfhmeo  20516  xrhmeo  20517  ovolval  20956  ovolf  20964  ovolctb  20972  itg2val  21205  mdegval  21532  mdegvalOLD  21533  mdegldg  21536  mdegxrf  21538  mdegcl  21539  aannenlem2  21794  nmooval  24162  nmoo0  24190  nmopval  25259  nmfnval  25279  nmop0  25389  nmfn0  25390  xrsupssd  26051  xrge0infssd  26053  xrsclat  26140  xrge0iifiso  26364  esumval  26499  esumnul  26501  esum0  26502  gsumesum  26509  esumsn  26514  esumpcvgval  26526  omsfval  26708  oms0  26709  mblfinlem2  28427  ovoliunnfl  28431  voliunnfl  28433  volsupnfl  28434  itg2addnclem  28441
  Copyright terms: Public domain W3C validator