Theorem xrltso 13055

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

Syntax hints:   Or wor 5531  ℝ^*cxr 11165   < clt 11166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-pre-lttri 11100  ax-pre-lttrn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171

This theorem is referenced by:  xrlttri2  13056  xrlttri3  13057  xrltne  13077  xmullem  13179  xmulasslem  13200  supxr  13228  supxrcl  13230  supxrun  13231  supxrmnf  13232  supxrunb1  13234  supxrunb2  13235  supxrub  13239  supxrlub  13240  xrsupssd  13248  infxrcl  13249  infxrlb  13250  infxrgelb  13251  xrinf0  13254  infmremnf  13259  limsupval  15397  limsupgval  15399  limsupgre  15404  ramval  16936  ramcl2lem  16937  prdsdsfn  17385  prdsdsval  17398  imasdsfn  17435  imasdsval  17436  prdsmet  24314  xpsdsval  24325  prdsbl  24435  tmsxpsval2  24483  nmoval  24659  xrge0tsms2  24780  metdsval  24792  iccpnfhmeo  24899  xrhmeo  24900  ovolval  25430  ovolf  25439  ovolctb  25447  itg2val  25685  mdegval  26024  mdegldg  26027  mdegxrf  26029  mdegcl  26030  aannenlem2  26293  nmooval  30838  nmoo0  30866  nmopval  31931  nmfnval  31951  nmop0  32061  nmfn0  32062  xrge0infssd  32841  infxrge0lb  32844  infxrge0glb  32845  infxrge0gelb  32846  xrsclat  33093  xrge0iifiso  34092  esumval  34203  esumnul  34205  esum0  34206  gsumesum  34216  esumsnf  34221  esumpcvgval  34235  esum2d  34250  omsfval  34451  omsf  34453  oms0  34454  omssubaddlem  34456  omssubadd  34457  mblfinlem2  37855  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  itg2addnclem  37868  radcnvrat  44551  infxrglb  45581  xrgtso  45586  infxr  45607  infxrunb2  45608  infxrpnf  45686  limsup0  45934  limsuppnfdlem  45941  limsupequzlem  45962  supcnvlimsup  45980  limsuplt2  45993  liminfval  45999  limsupge  46001  liminfgval  46002  liminfval2  46008  limsup10ex  46013  liminf10ex  46014  liminflelimsuplem  46015  cnrefiisplem  46069  etransclem48  46522  sge0val  46606  sge0z  46615  sge00  46616  sge0sn  46619  sge0tsms  46620  ovnval2  46785  smflimsuplem1  47060  smflimsuplem2  47061  smflimsuplem4  47063  smflimsuplem7  47066