Theorem xrltso 13297

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

This proof depends on syntax axioms:   Or wor 5562  ℝ^*cxr 11369   < clt 11370

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284  ax-pre-lttri 11301  ax-pre-lttrn 11302

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375

This theorem is used by:  xrlttri2  13298  xrlttri3  13299  xrltne  13319  xmullem  13421  xmulasslem  13442  supxr  13470  supxrcl  13472  supxrun  13473  supxrmnf  13474  supxrunb1  13476  supxrunb2  13477  supxrub  13481  supxrlub  13482  xrsupssd  13490  infxrcl  13491  infxrlb  13492  infxrgelb  13493  xrinf0  13496  infmremnf  13501  limsupval  15670  limsupgval  15672  limsupgre  15677  ramval  17215  ramcl2lem  17216  prdsdsfn  17665  prdsdsval  17678  imasdsfn  17715  imasdsval  17716  prdsmet  24719  xpsdsval  24730  prdsbl  24840  tmsxpsval2  24888  nmoval  25064  xrge0tsms2  25185  metdsval  25197  iccpnfhmeo  25296  xrhmeo  25297  ovolval  25824  ovolf  25833  ovolctb  25841  itg2val  26079  mdegval  26411  mdegldg  26414  mdegxrf  26416  mdegcl  26417  aannenlem2  26686  nmooval  31395  nmoo0  31423  nmopval  32488  nmfnval  32508  nmop0  32618  nmfn0  32619  xrge0infssd  33423  infxrge0lb  33426  infxrge0glb  33427  infxrge0gelb  33428  xrsclat  33642  xrge0iifiso  34637  esumval  34748  esumnul  34750  esum0  34751  gsumesum  34761  esumsnf  34766  esumpcvgval  34780  esum2d  34795  omsfval  34996  omsf  34998  oms0  34999  omssubaddlem  35001  omssubadd  35002  mblfinlem2  38768  ovoliunnfl  38772  voliunnfl  38774  volsupnfl  38775  itg2addnclem  38781  radcnvrat  45490  infxrglb  46557  xrgtso  46562  infxr  46583  infxrunb2  46584  infxrpnf  46661  limsup0  46909  limsuppnfdlem  46916  limsupequzlem  46937  supcnvlimsup  46955  limsuplt2  46968  liminfval  46974  limsupge  46976  liminfgval  46977  liminfval2  46983  limsup10ex  46988  liminf10ex  46989  liminflelimsuplem  46990  cnrefiisplem  47044  etransclem48  47497  sge0val  47581  sge0z  47590  sge00  47591  sge0sn  47594  sge0tsms  47595  ovnval2  47760  smflimsuplem1  48035  smflimsuplem2  48036  smflimsuplem4  48038  smflimsuplem7  48041