Theorem ltso 10986

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.

Step	Hyp	Ref	Expression
1		axlttri 10977	. 2 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 < 𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦 < 𝑥)))
2		lttr 10982	. 2 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧))
3	1, 2	isso2i 5529	1 ⊢ < Or ℝ

Syntax hints:   Or wor 5493  ℝcr 10801   < clt 10940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-pre-lttri 10876  ax-pre-lttrn 10877

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945

This theorem is referenced by:  gtso  10987  lttri2  10988  lttri3  10989  lttri4  10990  ltnr  11000  ltnsym2  11004  fimaxre  11849  fiminre  11852  lbinf  11858  suprcl  11865  suprub  11866  suprlub  11869  infrecl  11887  infregelb  11889  infrelb  11890  supfirege  11892  suprfinzcl  12365  uzinfi  12597  suprzcl2  12607  suprzub  12608  2resupmax  12851  infmrp1  13007  fseqsupcl  13625  ssnn0fi  13633  fsuppmapnn0fiublem  13638  isercolllem1  15304  isercolllem2  15305  summolem2  15356  zsum  15358  fsumcvg3  15369  mertenslem2  15525  prodmolem2  15573  zprod  15575  cnso  15884  gcdval  16131  dfgcd2  16182  lcmval  16225  lcmgcdlem  16239  odzval  16420  pczpre  16476  prmreclem1  16545  ramz  16654  odval  19057  odf  19060  gexval  19098  gsumval3  19423  retos  20735  mbfsup  24733  mbfinf  24734  itg2monolem1  24820  itg2mono  24823  dvgt0lem2  25072  dvgt0  25073  plyeq0lem  25276  dgrval  25294  dgrcl  25299  dgrub  25300  dgrlb  25302  elqaalem1  25384  elqaalem3  25386  aalioulem2  25398  logccv  25723  ex-po  28700  ssnnssfz  31010  lmdvg  31805  oddpwdc  32221  ballotlemi  32367  ballotlemiex  32368  ballotlemsup  32371  ballotlemimin  32372  ballotlemfrcn0  32396  ballotlemirc  32398  erdszelem3  33055  erdszelem4  33056  erdszelem5  33057  erdszelem6  33058  erdszelem8  33060  erdszelem9  33061  erdszelem11  33063  erdsze2lem1  33065  erdsze2lem2  33066  supfz  33600  inffz  33601  gtinf  34435  ptrecube  35704  poimirlem31  35735  poimirlem32  35736  heicant  35739  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  incsequz2  35834  totbndbnd  35874  prdsbnd  35878  aks4d1p4  40015  aks4d1p7  40019  sticksstones1  40030  sticksstones3  40032  pellfundval  40618  dgraaval  40885  dgraaf  40888  fzisoeu  42729  uzublem  42860  infrglb  43021  limsupubuzlem  43143  fourierdlem25  43563  fourierdlem31  43569  fourierdlem36  43574  fourierdlem37  43575  fourierdlem42  43580  fourierdlem79  43616  ioorrnopnlem  43735  hoicvr  43976  hoidmvlelem2  44024  iunhoiioolem  44103  vonioolem1  44108  prmdvdsfmtnof1lem1  44924  prmdvdsfmtnof  44926  prmdvdsfmtnof1  44927  ssnn0ssfz  45573  rrx2plordso  45958