Theorem xrltso 12521

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.

Step	Hyp	Ref	Expression
1		xrlttri 12519	. 2 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 < 𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦 < 𝑥)))
2		xrlttr 12520	. 2 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧))
3	1, 2	isso2i 5494	1 ⊢ < Or ℝ*

Syntax hints:   Or wor 5459  ℝ^*cxr 10660   < clt 10661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-cnex 10579  ax-resscn 10580  ax-pre-lttri 10597  ax-pre-lttrn 10598

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-po 5460  df-so 5461  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666

This theorem is referenced by:  xrlttri2  12522  xrlttri3  12523  xrltne  12543  xmullem  12644  xmulasslem  12665  supxr  12693  supxrcl  12695  supxrun  12696  supxrmnf  12697  supxrunb1  12699  supxrunb2  12700  supxrub  12704  supxrlub  12705  infxrcl  12713  infxrlb  12714  infxrgelb  12715  xrinf0  12718  infmremnf  12723  limsupval  14816  limsupgval  14818  limsupgre  14823  ramval  16327  ramcl2lem  16328  prdsdsfn  16721  prdsdsval  16734  imasdsfn  16770  imasdsval  16771  prdsmet  22963  xpsdsval  22974  prdsbl  23084  tmsxpsval2  23132  nmoval  23307  xrge0tsms2  23426  metdsval  23438  iccpnfhmeo  23532  xrhmeo  23533  ovolval  24057  ovolf  24066  ovolctb  24074  itg2val  24312  mdegval  24643  mdegldg  24646  mdegxrf  24648  mdegcl  24649  aannenlem2  24904  nmooval  28524  nmoo0  28552  nmopval  29617  nmfnval  29637  nmop0  29747  nmfn0  29748  xrsupssd  30469  xrge0infssd  30471  infxrge0lb  30474  infxrge0glb  30475  infxrge0gelb  30476  xrsclat  30674  xrge0iifiso  31185  esumval  31312  esumnul  31314  esum0  31315  gsumesum  31325  esumsnf  31330  esumpcvgval  31344  esum2d  31359  omsfval  31559  omsf  31561  oms0  31562  omssubaddlem  31564  omssubadd  31565  mblfinlem2  34964  ovoliunnfl  34968  voliunnfl  34970  volsupnfl  34971  itg2addnclem  34977  radcnvrat  40736  infxrglb  41698  xrgtso  41703  infxr  41725  infxrunb2  41726  infxrpnf  41811  limsup0  42065  limsuppnfdlem  42072  limsupequzlem  42093  supcnvlimsup  42111  limsuplt2  42124  liminfval  42130  limsupge  42132  liminfgval  42133  liminfval2  42139  limsup10ex  42144  liminf10ex  42145  liminflelimsuplem  42146  cnrefiisplem  42200  etransclem48  42657  sge0val  42738  sge0z  42747  sge00  42748  sge0sn  42751  sge0tsms  42752  ovnval2  42917  smflimsuplem1  43184  smflimsuplem2  43185  smflimsuplem4  43187  smflimsuplem7  43190