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

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

Proof of Theorem xrltso
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrlttri 12524 . 2 ((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) → (𝑥 < 𝑦 ↔ ¬ (𝑥 = 𝑦𝑦 < 𝑥)))
2 xrlttr 12525 . 2 ((𝑥 ∈ ℝ*𝑦 ∈ ℝ*𝑧 ∈ ℝ*) → ((𝑥 < 𝑦𝑦 < 𝑧) → 𝑥 < 𝑧))
31, 2isso2i 5501 1 < Or ℝ*
Colors of variables: wff setvar class
Syntax hints:   Or wor 5466  *cxr 10666   < clt 10667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-pre-lttri 10603  ax-pre-lttrn 10604
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672
This theorem is referenced by:  xrlttri2  12527  xrlttri3  12528  xrltne  12548  xmullem  12649  xmulasslem  12670  supxr  12698  supxrcl  12700  supxrun  12701  supxrmnf  12702  supxrunb1  12704  supxrunb2  12705  supxrub  12709  supxrlub  12710  infxrcl  12718  infxrlb  12719  infxrgelb  12720  xrinf0  12723  infmremnf  12728  limsupval  14823  limsupgval  14825  limsupgre  14830  ramval  16336  ramcl2lem  16337  prdsdsfn  16730  prdsdsval  16743  imasdsfn  16779  imasdsval  16780  prdsmet  22972  xpsdsval  22983  prdsbl  23093  tmsxpsval2  23141  nmoval  23316  xrge0tsms2  23435  metdsval  23447  iccpnfhmeo  23541  xrhmeo  23542  ovolval  24066  ovolf  24075  ovolctb  24083  itg2val  24321  mdegval  24649  mdegldg  24652  mdegxrf  24654  mdegcl  24655  aannenlem2  24910  nmooval  28532  nmoo0  28560  nmopval  29625  nmfnval  29645  nmop0  29755  nmfn0  29756  xrsupssd  30475  xrge0infssd  30477  infxrge0lb  30480  infxrge0glb  30481  infxrge0gelb  30482  xrsclat  30660  xrge0iifiso  31166  esumval  31293  esumnul  31295  esum0  31296  gsumesum  31306  esumsnf  31311  esumpcvgval  31325  esum2d  31340  omsfval  31540  omsf  31542  oms0  31543  omssubaddlem  31545  omssubadd  31546  mblfinlem2  34917  ovoliunnfl  34921  voliunnfl  34923  volsupnfl  34924  itg2addnclem  34930  radcnvrat  40631  infxrglb  41592  xrgtso  41597  infxr  41619  infxrunb2  41620  infxrpnf  41705  limsup0  41959  limsuppnfdlem  41966  limsupequzlem  41987  supcnvlimsup  42005  limsuplt2  42018  liminfval  42024  limsupge  42026  liminfgval  42027  liminfval2  42033  limsup10ex  42038  liminf10ex  42039  liminflelimsuplem  42040  cnrefiisplem  42094  etransclem48  42552  sge0val  42633  sge0z  42642  sge00  42643  sge0sn  42646  sge0tsms  42647  ovnval2  42812  smflimsuplem1  43079  smflimsuplem2  43080  smflimsuplem4  43082  smflimsuplem7  43085
  Copyright terms: Public domain W3C validator