MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltso Structured version   Unicode version

Theorem ltso 9594
Description: 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
Assertion
Ref Expression
ltso  |-  <  Or  RR

Proof of Theorem ltso
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axlttri 9585 . 2  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  <  y  <->  -.  ( x  =  y  \/  y  <  x
) ) )
2 lttr 9590 . 2  |-  ( ( x  e.  RR  /\  y  e.  RR  /\  z  e.  RR )  ->  (
( x  <  y  /\  y  <  z )  ->  x  <  z
) )
31, 2isso2i 4759 1  |-  <  Or  RR
Colors of variables: wff setvar class
Syntax hints:    Or wor 4726   RRcr 9420    < clt 9557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-resscn 9478  ax-pre-lttri 9495  ax-pre-lttrn 9496
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-po 4727  df-so 4728  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-pnf 9559  df-mnf 9560  df-ltxr 9562
This theorem is referenced by:  gtso  9595  lttri2  9596  lttri3  9597  lttri4  9598  ltnr  9608  ltnsym2  9613  fimaxre  10424  suprcl  10437  suprub  10438  suprlub  10439  supfirege  10459  suprfinzcl  10912  suprzcl2  11109  suprzub  11110  fseqsupcl  12009  ssnn0fi  12016  fsuppmapnn0fiublem  12018  isercolllem1  13508  isercolllem2  13509  summolem2  13559  zsum  13561  fsumcvg3  13572  mertenslem2  13715  prodmolem2  13763  zprod  13765  cnso  14001  gcdval  14167  pczpre  14392  prmreclem1  14455  ramz  14564  gsumval3OLD  17044  gsumval3  17047  retos  18764  mbfsup  22175  mbfinf  22176  itg2monolem1  22261  itg2mono  22264  dvgt0lem2  22508  dvgt0  22509  plyeq0lem  22711  dgrval  22729  dgrcl  22734  dgrub  22735  dgrlb  22737  logccv  23150  ex-po  25298  ssnnssfz  27780  lmdvg  28120  oddpwdc  28512  erdszelem3  28862  erdszelem4  28863  erdszelem5  28864  erdszelem6  28865  erdszelem8  28867  erdszelem9  28868  erdszelem11  28870  erdsze2lem1  28872  erdsze2lem2  28873  supfz  29309  inffz  29310  mblfinlem3  30254  mblfinlem4  30255  ismblfin  30256  incsequz2  30444  totbndbnd  30487  prdsbnd  30491  fzisoeu  31701  fourierdlem25  32115  fourierdlem31  32121  fourierdlem36  32126  fourierdlem37  32127  fourierdlem42  32132  fourierdlem79  32169  ssnn0ssfz  33173
  Copyright terms: Public domain W3C validator