Theorem xrltso 13273

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

This proof depends on syntax axioms:   Or wor 5557  ℝ^*cxr 11345   < clt 11346

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260  ax-pre-lttri 11277  ax-pre-lttrn 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351

This theorem is used by:  xrlttri2  13274  xrlttri3  13275  xrltne  13295  xmullem  13397  xmulasslem  13418  supxr  13446  supxrcl  13448  supxrun  13449  supxrmnf  13450  supxrunb1  13452  supxrunb2  13453  supxrub  13457  supxrlub  13458  xrsupssd  13466  infxrcl  13467  infxrlb  13468  infxrgelb  13469  xrinf0  13472  infmremnf  13477  limsupval  15646  limsupgval  15648  limsupgre  15653  ramval  17191  ramcl2lem  17192  prdsdsfn  17641  prdsdsval  17654  imasdsfn  17691  imasdsval  17692  prdsmet  24694  xpsdsval  24705  prdsbl  24815  tmsxpsval2  24863  nmoval  25039  xrge0tsms2  25160  metdsval  25172  iccpnfhmeo  25271  xrhmeo  25272  ovolval  25799  ovolf  25808  ovolctb  25816  itg2val  26054  mdegval  26386  mdegldg  26389  mdegxrf  26391  mdegcl  26392  aannenlem2  26661  nmooval  31370  nmoo0  31398  nmopval  32463  nmfnval  32483  nmop0  32593  nmfn0  32594  xrge0infssd  33399  infxrge0lb  33402  infxrge0glb  33403  infxrge0gelb  33404  xrsclat  33618  xrge0iifiso  34613  esumval  34724  esumnul  34726  esum0  34727  gsumesum  34737  esumsnf  34742  esumpcvgval  34756  esum2d  34771  omsfval  34972  omsf  34974  oms0  34975  omssubaddlem  34977  omssubadd  34978  mblfinlem2  38669  ovoliunnfl  38673  voliunnfl  38675  volsupnfl  38676  itg2addnclem  38682  radcnvrat  45391  infxrglb  46445  xrgtso  46450  infxr  46471  infxrunb2  46472  infxrpnf  46549  limsup0  46797  limsuppnfdlem  46804  limsupequzlem  46825  supcnvlimsup  46843  limsuplt2  46856  liminfval  46862  limsupge  46864  liminfgval  46865  liminfval2  46871  limsup10ex  46876  liminf10ex  46877  liminflelimsuplem  46878  cnrefiisplem  46932  etransclem48  47385  sge0val  47469  sge0z  47478  sge00  47479  sge0sn  47482  sge0tsms  47483  ovnval2  47648  smflimsuplem1  47923  smflimsuplem2  47924  smflimsuplem4  47926  smflimsuplem7  47929