Theorem xrltso 13196

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

This proof depends on syntax axioms:   Or wor 5566  ℝ^*cxr 11270   < clt 11271

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-pre-lttri 11202  ax-pre-lttrn 11203

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276

This theorem is used by:  xrlttri2  13197  xrlttri3  13198  xrltne  13218  xmullem  13320  xmulasslem  13341  supxr  13369  supxrcl  13371  supxrun  13372  supxrmnf  13373  supxrunb1  13375  supxrunb2  13376  supxrub  13380  supxrlub  13381  xrsupssd  13389  infxrcl  13390  infxrlb  13391  infxrgelb  13392  xrinf0  13395  infmremnf  13400  limsupval  15565  limsupgval  15567  limsupgre  15572  ramval  17106  ramcl2lem  17107  prdsdsfn  17556  prdsdsval  17569  imasdsfn  17606  imasdsval  17607  prdsmet  24602  xpsdsval  24613  prdsbl  24723  tmsxpsval2  24771  nmoval  24947  xrge0tsms2  25068  metdsval  25080  iccpnfhmeo  25179  xrhmeo  25180  ovolval  25707  ovolf  25716  ovolctb  25724  itg2val  25962  mdegval  26295  mdegldg  26298  mdegxrf  26300  mdegcl  26301  aannenlem2  26572  nmooval  31252  nmoo0  31280  nmopval  32345  nmfnval  32365  nmop0  32475  nmfn0  32476  xrge0infssd  33240  infxrge0lb  33243  infxrge0glb  33244  infxrge0gelb  33245  xrsclat  33459  xrge0iifiso  34453  esumval  34564  esumnul  34566  esum0  34567  gsumesum  34577  esumsnf  34582  esumpcvgval  34596  esum2d  34611  omsfval  34813  omsf  34815  oms0  34816  omssubaddlem  34818  omssubadd  34819  mblfinlem2  38415  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  itg2addnclem  38428  radcnvrat  45146  infxrglb  46178  xrgtso  46183  infxr  46204  infxrunb2  46205  infxrpnf  46282  limsup0  46530  limsuppnfdlem  46537  limsupequzlem  46558  supcnvlimsup  46576  limsuplt2  46589  liminfval  46595  limsupge  46597  liminfgval  46598  liminfval2  46604  limsup10ex  46609  liminf10ex  46610  liminflelimsuplem  46611  cnrefiisplem  46665  etransclem48  47118  sge0val  47202  sge0z  47211  sge00  47212  sge0sn  47215  sge0tsms  47216  ovnval2  47381  smflimsuplem1  47656  smflimsuplem2  47657  smflimsuplem4  47659  smflimsuplem7  47662