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

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

Proof of Theorem ltso
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axlttri 10701 . 2 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 < 𝑦 ↔ ¬ (𝑥 = 𝑦𝑦 < 𝑥)))
2 lttr 10706 . 2 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 < 𝑦𝑦 < 𝑧) → 𝑥 < 𝑧))
31, 2isso2i 5485 1 < Or ℝ
Colors of variables: wff setvar class
Syntax hints:   Or wor 5450  cr 10525   < clt 10664
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-resscn 10583  ax-pre-lttri 10600  ax-pre-lttrn 10601
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-po 5451  df-so 5452  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10666  df-mnf 10667  df-ltxr 10669
This theorem is referenced by:  gtso  10711  lttri2  10712  lttri3  10713  lttri4  10714  ltnr  10724  ltnsym2  10728  fimaxre  11573  fiminre  11576  lbinf  11581  suprcl  11588  suprub  11589  suprlub  11592  infrecl  11610  infregelb  11612  infrelb  11613  supfirege  11614  suprfinzcl  12085  uzinfi  12316  suprzcl2  12326  suprzub  12327  2resupmax  12569  infmrp1  12725  fseqsupcl  13340  ssnn0fi  13348  fsuppmapnn0fiublem  13353  isercolllem1  15012  isercolllem2  15013  summolem2  15064  zsum  15066  fsumcvg3  15077  mertenslem2  15232  prodmolem2  15280  zprod  15282  cnso  15591  gcdval  15834  dfgcd2  15883  lcmval  15925  lcmgcdlem  15939  odzval  16117  pczpre  16173  prmreclem1  16241  ramz  16350  odval  18653  odf  18656  gexval  18694  gsumval3  19018  retos  20305  mbfsup  24266  mbfinf  24267  itg2monolem1  24352  itg2mono  24355  dvgt0lem2  24604  dvgt0  24605  plyeq0lem  24805  dgrval  24823  dgrcl  24828  dgrub  24829  dgrlb  24831  elqaalem1  24913  elqaalem3  24915  aalioulem2  24927  logccv  25252  ex-po  28218  ssnnssfz  30520  lmdvg  31270  oddpwdc  31686  ballotlemi  31832  ballotlemiex  31833  ballotlemsup  31836  ballotlemimin  31837  ballotlemfrcn0  31861  ballotlemirc  31863  erdszelem3  32514  erdszelem4  32515  erdszelem5  32516  erdszelem6  32517  erdszelem8  32519  erdszelem9  32520  erdszelem11  32522  erdsze2lem1  32524  erdsze2lem2  32525  supfz  33034  inffz  33035  gtinf  33741  ptrecube  35019  poimirlem31  35050  poimirlem32  35051  heicant  35054  mblfinlem3  35058  mblfinlem4  35059  ismblfin  35060  incsequz2  35149  totbndbnd  35189  prdsbnd  35193  pellfundval  39755  dgraaval  40022  dgraaf  40025  fzisoeu  41875  uzublem  42010  infrglb  42175  limsupubuzlem  42297  fourierdlem25  42717  fourierdlem31  42723  fourierdlem36  42728  fourierdlem37  42729  fourierdlem42  42734  fourierdlem79  42770  ioorrnopnlem  42889  hoicvr  43130  hoidmvlelem2  43178  iunhoiioolem  43257  vonioolem1  43262  prmdvdsfmtnof1lem1  44044  prmdvdsfmtnof  44046  prmdvdsfmtnof1  44047  ssnn0ssfz  44694  rrx2plordso  45081
  Copyright terms: Public domain W3C validator