Theorem xrltso 13167

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 13165	. 2 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 < 𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦 < 𝑥)))
2		xrlttr 13166	. 2 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧))
3	1, 2	isso2i 5608	1 ⊢ < Or ℝ*

Syntax hints:   Or wor 5570  ℝ^*cxr 11243   < clt 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-pre-lttri 11175  ax-pre-lttrn 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249

This theorem is referenced by:  xrlttri2  13168  xrlttri3  13169  xrltne  13189  xmullem  13291  xmulasslem  13312  supxr  13340  supxrcl  13342  supxrun  13343  supxrmnf  13344  supxrunb1  13346  supxrunb2  13347  supxrub  13351  supxrlub  13352  xrsupssd  13360  infxrcl  13361  infxrlb  13362  infxrgelb  13363  xrinf0  13366  infmremnf  13371  limsupval  15527  limsupgval  15529  limsupgre  15534  ramval  17069  ramcl2lem  17070  prdsdsfn  17519  prdsdsval  17532  imasdsfn  17569  imasdsval  17570  prdsmet  24508  xpsdsval  24519  prdsbl  24629  tmsxpsval2  24677  nmoval  24853  xrge0tsms2  24974  metdsval  24986  iccpnfhmeo  25085  xrhmeo  25086  ovolval  25613  ovolf  25622  ovolctb  25630  itg2val  25868  mdegval  26201  mdegldg  26204  mdegxrf  26206  mdegcl  26207  aannenlem2  26471  nmooval  31093  nmoo0  31121  nmopval  32186  nmfnval  32206  nmop0  32316  nmfn0  32317  xrge0infssd  33084  infxrge0lb  33087  infxrge0glb  33088  infxrge0gelb  33089  xrsclat  33309  xrge0iifiso  34303  esumval  34414  esumnul  34416  esum0  34417  gsumesum  34427  esumsnf  34432  esumpcvgval  34446  esum2d  34461  omsfval  34662  omsf  34664  oms0  34665  omssubaddlem  34667  omssubadd  34668  mblfinlem2  38287  ovoliunnfl  38291  voliunnfl  38293  volsupnfl  38294  itg2addnclem  38300  radcnvrat  45004  infxrglb  46036  xrgtso  46041  infxr  46062  infxrunb2  46063  infxrpnf  46140  limsup0  46388  limsuppnfdlem  46395  limsupequzlem  46416  supcnvlimsup  46434  limsuplt2  46447  liminfval  46453  limsupge  46455  liminfgval  46456  liminfval2  46462  limsup10ex  46467  liminf10ex  46468  liminflelimsuplem  46469  cnrefiisplem  46523  etransclem48  46976  sge0val  47060  sge0z  47069  sge00  47070  sge0sn  47073  sge0tsms  47074  ovnval2  47239  smflimsuplem1  47514  smflimsuplem2  47515  smflimsuplem4  47517  smflimsuplem7  47520