Theorem xrltso 13101

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

Syntax hints:   Or wor 5545  ℝ^*cxr 11207   < clt 11208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-pre-lttri 11142  ax-pre-lttrn 11143

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213

This theorem is referenced by:  xrlttri2  13102  xrlttri3  13103  xrltne  13123  xmullem  13224  xmulasslem  13245  supxr  13273  supxrcl  13275  supxrun  13276  supxrmnf  13277  supxrunb1  13279  supxrunb2  13280  supxrub  13284  supxrlub  13285  xrsupssd  13293  infxrcl  13294  infxrlb  13295  infxrgelb  13296  xrinf0  13299  infmremnf  13304  limsupval  15440  limsupgval  15442  limsupgre  15447  ramval  16979  ramcl2lem  16980  prdsdsfn  17428  prdsdsval  17441  imasdsfn  17477  imasdsval  17478  prdsmet  24258  xpsdsval  24269  prdsbl  24379  tmsxpsval2  24427  nmoval  24603  xrge0tsms2  24724  metdsval  24736  iccpnfhmeo  24843  xrhmeo  24844  ovolval  25374  ovolf  25383  ovolctb  25391  itg2val  25629  mdegval  25968  mdegldg  25971  mdegxrf  25973  mdegcl  25974  aannenlem2  26237  nmooval  30692  nmoo0  30720  nmopval  31785  nmfnval  31805  nmop0  31915  nmfn0  31916  xrge0infssd  32684  infxrge0lb  32687  infxrge0glb  32688  infxrge0gelb  32689  xrsclat  32949  xrge0iifiso  33925  esumval  34036  esumnul  34038  esum0  34039  gsumesum  34049  esumsnf  34054  esumpcvgval  34068  esum2d  34083  omsfval  34285  omsf  34287  oms0  34288  omssubaddlem  34290  omssubadd  34291  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  itg2addnclem  37665  radcnvrat  44303  infxrglb  45336  xrgtso  45341  infxr  45363  infxrunb2  45364  infxrpnf  45442  limsup0  45692  limsuppnfdlem  45699  limsupequzlem  45720  supcnvlimsup  45738  limsuplt2  45751  liminfval  45757  limsupge  45759  liminfgval  45760  liminfval2  45766  limsup10ex  45771  liminf10ex  45772  liminflelimsuplem  45773  cnrefiisplem  45827  etransclem48  46280  sge0val  46364  sge0z  46373  sge00  46374  sge0sn  46377  sge0tsms  46378  ovnval2  46543  smflimsuplem1  46818  smflimsuplem2  46819  smflimsuplem4  46821  smflimsuplem7  46824