Theorem xrltso 13184

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

Syntax hints:   Or wor 5590  ℝ^*cxr 11295   < clt 11296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-pre-lttri 11230  ax-pre-lttrn 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-po 5591  df-so 5592  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-er 8746  df-en 8987  df-dom 8988  df-sdom 8989  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301

This theorem is referenced by:  xrlttri2  13185  xrlttri3  13186  xrltne  13206  xmullem  13307  xmulasslem  13328  supxr  13356  supxrcl  13358  supxrun  13359  supxrmnf  13360  supxrunb1  13362  supxrunb2  13363  supxrub  13367  supxrlub  13368  infxrcl  13376  infxrlb  13377  infxrgelb  13378  xrinf0  13381  infmremnf  13386  limsupval  15511  limsupgval  15513  limsupgre  15518  ramval  17047  ramcl2lem  17048  prdsdsfn  17511  prdsdsval  17524  imasdsfn  17560  imasdsval  17561  prdsmet  24381  xpsdsval  24392  prdsbl  24505  tmsxpsval2  24553  nmoval  24737  xrge0tsms2  24858  metdsval  24870  iccpnfhmeo  24977  xrhmeo  24978  ovolval  25509  ovolf  25518  ovolctb  25526  itg2val  25764  mdegval  26103  mdegldg  26106  mdegxrf  26108  mdegcl  26109  aannenlem2  26372  nmooval  30783  nmoo0  30811  nmopval  31876  nmfnval  31896  nmop0  32006  nmfn0  32007  xrsupssd  32764  xrge0infssd  32766  infxrge0lb  32769  infxrge0glb  32770  infxrge0gelb  32771  xrsclat  33014  xrge0iifiso  33935  esumval  34048  esumnul  34050  esum0  34051  gsumesum  34061  esumsnf  34066  esumpcvgval  34080  esum2d  34095  omsfval  34297  omsf  34299  oms0  34300  omssubaddlem  34302  omssubadd  34303  mblfinlem2  37666  ovoliunnfl  37670  voliunnfl  37672  volsupnfl  37673  itg2addnclem  37679  radcnvrat  44338  infxrglb  45356  xrgtso  45361  infxr  45383  infxrunb2  45384  infxrpnf  45462  limsup0  45714  limsuppnfdlem  45721  limsupequzlem  45742  supcnvlimsup  45760  limsuplt2  45773  liminfval  45779  limsupge  45781  liminfgval  45782  liminfval2  45788  limsup10ex  45793  liminf10ex  45794  liminflelimsuplem  45795  cnrefiisplem  45849  etransclem48  46302  sge0val  46386  sge0z  46395  sge00  46396  sge0sn  46399  sge0tsms  46400  ovnval2  46565  smflimsuplem1  46840  smflimsuplem2  46841  smflimsuplem4  46843  smflimsuplem7  46846