Theorem xrltso 13070

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

Syntax hints:   Or wor 5549  ℝ^*cxr 11197   < clt 11198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117  ax-pre-lttri 11134  ax-pre-lttrn 11135

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  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 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203

This theorem is referenced by:  xrlttri2  13071  xrlttri3  13072  xrltne  13092  xmullem  13193  xmulasslem  13214  supxr  13242  supxrcl  13244  supxrun  13245  supxrmnf  13246  supxrunb1  13248  supxrunb2  13249  supxrub  13253  supxrlub  13254  infxrcl  13262  infxrlb  13263  infxrgelb  13264  xrinf0  13267  infmremnf  13272  limsupval  15368  limsupgval  15370  limsupgre  15375  ramval  16891  ramcl2lem  16892  prdsdsfn  17361  prdsdsval  17374  imasdsfn  17410  imasdsval  17411  prdsmet  23760  xpsdsval  23771  prdsbl  23884  tmsxpsval2  23932  nmoval  24116  xrge0tsms2  24235  metdsval  24247  iccpnfhmeo  24345  xrhmeo  24346  ovolval  24874  ovolf  24883  ovolctb  24891  itg2val  25130  mdegval  25465  mdegldg  25468  mdegxrf  25470  mdegcl  25471  aannenlem2  25726  nmooval  29768  nmoo0  29796  nmopval  30861  nmfnval  30881  nmop0  30991  nmfn0  30992  xrsupssd  31732  xrge0infssd  31734  infxrge0lb  31737  infxrge0glb  31738  infxrge0gelb  31739  xrsclat  31941  xrge0iifiso  32605  esumval  32734  esumnul  32736  esum0  32737  gsumesum  32747  esumsnf  32752  esumpcvgval  32766  esum2d  32781  omsfval  32983  omsf  32985  oms0  32986  omssubaddlem  32988  omssubadd  32989  mblfinlem2  36189  ovoliunnfl  36193  voliunnfl  36195  volsupnfl  36196  itg2addnclem  36202  radcnvrat  42716  infxrglb  43695  xrgtso  43700  infxr  43722  infxrunb2  43723  infxrpnf  43801  limsup0  44055  limsuppnfdlem  44062  limsupequzlem  44083  supcnvlimsup  44101  limsuplt2  44114  liminfval  44120  limsupge  44122  liminfgval  44123  liminfval2  44129  limsup10ex  44134  liminf10ex  44135  liminflelimsuplem  44136  cnrefiisplem  44190  etransclem48  44643  sge0val  44727  sge0z  44736  sge00  44737  sge0sn  44740  sge0tsms  44741  ovnval2  44906  smflimsuplem1  45181  smflimsuplem2  45182  smflimsuplem4  45184  smflimsuplem7  45187