Theorem xrltso 13116

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-pre-lttri 11180  ax-pre-lttrn 11181

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249

This theorem is referenced by:  xrlttri2  13117  xrlttri3  13118  xrltne  13138  xmullem  13239  xmulasslem  13260  supxr  13288  supxrcl  13290  supxrun  13291  supxrmnf  13292  supxrunb1  13294  supxrunb2  13295  supxrub  13299  supxrlub  13300  infxrcl  13308  infxrlb  13309  infxrgelb  13310  xrinf0  13313  infmremnf  13318  limsupval  15414  limsupgval  15416  limsupgre  15421  ramval  16937  ramcl2lem  16938  prdsdsfn  17407  prdsdsval  17420  imasdsfn  17456  imasdsval  17457  prdsmet  23867  xpsdsval  23878  prdsbl  23991  tmsxpsval2  24039  nmoval  24223  xrge0tsms2  24342  metdsval  24354  iccpnfhmeo  24452  xrhmeo  24453  ovolval  24981  ovolf  24990  ovolctb  24998  itg2val  25237  mdegval  25572  mdegldg  25575  mdegxrf  25577  mdegcl  25578  aannenlem2  25833  nmooval  30003  nmoo0  30031  nmopval  31096  nmfnval  31116  nmop0  31226  nmfn0  31227  xrsupssd  31959  xrge0infssd  31961  infxrge0lb  31964  infxrge0glb  31965  infxrge0gelb  31966  xrsclat  32168  xrge0iifiso  32903  esumval  33032  esumnul  33034  esum0  33035  gsumesum  33045  esumsnf  33050  esumpcvgval  33064  esum2d  33079  omsfval  33281  omsf  33283  oms0  33284  omssubaddlem  33286  omssubadd  33287  mblfinlem2  36514  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  itg2addnclem  36527  radcnvrat  43058  infxrglb  44036  xrgtso  44041  infxr  44063  infxrunb2  44064  infxrpnf  44142  limsup0  44396  limsuppnfdlem  44403  limsupequzlem  44424  supcnvlimsup  44442  limsuplt2  44455  liminfval  44461  limsupge  44463  liminfgval  44464  liminfval2  44470  limsup10ex  44475  liminf10ex  44476  liminflelimsuplem  44477  cnrefiisplem  44531  etransclem48  44984  sge0val  45068  sge0z  45077  sge00  45078  sge0sn  45081  sge0tsms  45082  ovnval2  45247  smflimsuplem1  45522  smflimsuplem2  45523  smflimsuplem4  45525  smflimsuplem7  45528