Theorem xrltso 12188

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

Syntax hints:   Or wor 5187  ℝ^*cxr 10286   < clt 10287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-cnex 10205  ax-resscn 10206  ax-pre-lttri 10223  ax-pre-lttrn 10224

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-nel 3037  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-po 5188  df-so 5189  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-er 7914  df-en 8125  df-dom 8126  df-sdom 8127  df-pnf 10289  df-mnf 10290  df-xr 10291  df-ltxr 10292

This theorem is referenced by:  xrlttri2  12189  xrlttri3  12190  xrltne  12208  xmullem  12308  xmulasslem  12329  supxr  12357  supxrcl  12359  supxrun  12360  supxrmnf  12361  supxrunb1  12363  supxrunb2  12364  supxrub  12368  supxrlub  12369  infxrcl  12377  infxrlb  12378  infxrgelb  12379  xrinf0  12382  infmremnf  12387  limsupval  14425  limsupgval  14427  limsupgre  14432  ramval  15935  ramcl2lem  15936  prdsdsfn  16348  prdsdsval  16361  imasdsfn  16397  imasdsval  16398  prdsmet  22397  xpsdsval  22408  prdsbl  22518  tmsxpsval2  22566  nmoval  22741  xrge0tsms2  22860  metdsval  22872  iccpnfhmeo  22966  xrhmeo  22967  ovolval  23463  ovolf  23471  ovolctb  23479  itg2val  23715  mdegval  24043  mdegldg  24046  mdegxrf  24048  mdegcl  24049  aannenlem2  24304  nmooval  27949  nmoo0  27977  nmopval  29046  nmfnval  29066  nmop0  29176  nmfn0  29177  xrsupssd  29855  xrge0infssd  29857  infxrge0lb  29860  infxrge0glb  29861  infxrge0gelb  29862  xrsclat  30011  xrge0iifiso  30312  esumval  30439  esumnul  30441  esum0  30442  gsumesum  30452  esumsnf  30457  esumpcvgval  30471  esum2d  30486  omsfval  30687  omsf  30689  oms0  30690  omssubaddlem  30692  omssubadd  30693  mblfinlem2  33779  ovoliunnfl  33783  voliunnfl  33785  volsupnfl  33786  itg2addnclem  33793  radcnvrat  39034  infxrglb  40073  xrgtso  40078  infxr  40100  infxrunb2  40101  infxrpnf  40191  limsup0  40448  limsuppnfdlem  40455  limsupequzlem  40476  supcnvlimsup  40494  limsuplt2  40507  liminfval  40513  limsupge  40515  liminfgval  40516  liminfval2  40522  limsup10ex  40527  liminf10ex  40528  liminflelimsuplem  40529  cnrefiisplem  40577  etransclem48  41021  sge0val  41105  sge0z  41114  sge00  41115  sge0sn  41118  sge0tsms  41119  ovnval2  41284  smflimsuplem1  41551  smflimsuplem2  41552  smflimsuplem4  41554  smflimsuplem7  41557