Theorem xrltso 12533

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

Syntax hints:   Or wor 5472  ℝ^*cxr 10673   < clt 10674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-cnex 10592  ax-resscn 10593  ax-pre-lttri 10610  ax-pre-lttrn 10611

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  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 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-po 5473  df-so 5474  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679

This theorem is referenced by:  xrlttri2  12534  xrlttri3  12535  xrltne  12555  xmullem  12656  xmulasslem  12677  supxr  12705  supxrcl  12707  supxrun  12708  supxrmnf  12709  supxrunb1  12711  supxrunb2  12712  supxrub  12716  supxrlub  12717  infxrcl  12725  infxrlb  12726  infxrgelb  12727  xrinf0  12730  infmremnf  12735  limsupval  14830  limsupgval  14832  limsupgre  14837  ramval  16343  ramcl2lem  16344  prdsdsfn  16737  prdsdsval  16750  imasdsfn  16786  imasdsval  16787  prdsmet  22979  xpsdsval  22990  prdsbl  23100  tmsxpsval2  23148  nmoval  23323  xrge0tsms2  23442  metdsval  23454  iccpnfhmeo  23548  xrhmeo  23549  ovolval  24073  ovolf  24082  ovolctb  24090  itg2val  24328  mdegval  24656  mdegldg  24659  mdegxrf  24661  mdegcl  24662  aannenlem2  24917  nmooval  28539  nmoo0  28567  nmopval  29632  nmfnval  29652  nmop0  29762  nmfn0  29763  xrsupssd  30482  xrge0infssd  30484  infxrge0lb  30487  infxrge0glb  30488  infxrge0gelb  30489  xrsclat  30667  xrge0iifiso  31178  esumval  31305  esumnul  31307  esum0  31308  gsumesum  31318  esumsnf  31323  esumpcvgval  31337  esum2d  31352  omsfval  31552  omsf  31554  oms0  31555  omssubaddlem  31557  omssubadd  31558  mblfinlem2  34929  ovoliunnfl  34933  voliunnfl  34935  volsupnfl  34936  itg2addnclem  34942  radcnvrat  40644  infxrglb  41606  xrgtso  41611  infxr  41633  infxrunb2  41634  infxrpnf  41719  limsup0  41973  limsuppnfdlem  41980  limsupequzlem  42001  supcnvlimsup  42019  limsuplt2  42032  liminfval  42038  limsupge  42040  liminfgval  42041  liminfval2  42047  limsup10ex  42052  liminf10ex  42053  liminflelimsuplem  42054  cnrefiisplem  42108  etransclem48  42566  sge0val  42647  sge0z  42656  sge00  42657  sge0sn  42660  sge0tsms  42661  ovnval2  42826  smflimsuplem1  43093  smflimsuplem2  43094  smflimsuplem4  43096  smflimsuplem7  43099