Theorem ltso 11217

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 11208	. 2 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 < 𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦 < 𝑥)))
2		lttr 11213	. 2 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧))
3	1, 2	isso2i 5563	1 ⊢ < Or ℝ

Syntax hints:   Or wor 5525  ℝcr 11028   < clt 11170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-pre-lttri 11103  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-po 5526  df-so 5527  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  gtso  11218  lttri2  11219  lttri3  11220  lttri4  11221  ltnr  11232  ltnsym2  11236  fimaxre  12091  fiminre  12094  lbinf  12100  suprcl  12107  suprub  12108  suprlub  12111  infrecl  12129  infregelb  12131  infrelb  12132  supfirege  12134  suprfinzcl  12634  uzinfi  12869  suprzcl2  12879  suprzub  12880  2resupmax  13131  infmrp1  13288  fseqsupcl  13930  ssnn0fi  13938  fsuppmapnn0fiublem  13943  isercolllem1  15618  isercolllem2  15619  summolem2  15669  zsum  15671  fsumcvg3  15682  mertenslem2  15841  prodmolem2  15891  zprod  15893  cnso  16205  gcdval  16456  dfgcd2  16506  lcmval  16552  lcmgcdlem  16566  odzval  16753  pczpre  16809  prmreclem1  16878  ramz  16987  odval  19500  odf  19503  gexval  19544  gsumval3  19873  retos  21593  mbfsup  25649  mbfinf  25650  itg2monolem1  25735  itg2mono  25738  dvgt0lem2  25988  dvgt0  25989  plyeq0lem  26193  dgrval  26211  dgrcl  26216  dgrub  26217  dgrlb  26219  elqaalem1  26303  elqaalem3  26305  aalioulem2  26317  logccv  26645  ex-po  30523  ssnnssfz  32879  lmdvg  34137  oddpwdc  34538  ballotlemi  34685  ballotlemiex  34686  ballotlemsup  34689  ballotlemimin  34690  ballotlemfrcn0  34714  ballotlemirc  34716  erdszelem3  35421  erdszelem4  35422  erdszelem5  35423  erdszelem6  35424  erdszelem8  35426  erdszelem9  35427  erdszelem11  35429  erdsze2lem1  35431  erdsze2lem2  35432  supfz  35957  inffz  35958  gtinf  36547  ptrecube  37987  poimirlem31  38018  poimirlem32  38019  heicant  38022  mblfinlem3  38026  mblfinlem4  38027  ismblfin  38028  incsequz2  38116  totbndbnd  38156  prdsbnd  38160  aks4d1p4  42564  aks4d1p7  42568  sticksstones1  42631  sticksstones3  42633  sn-suprcld  42983  sn-suprubd  42984  pellfundval  43325  dgraaval  43589  dgraaf  43592  fzisoeu  45748  uzublem  45873  infrglb  46035  limsupubuzlem  46155  fourierdlem25  46575  fourierdlem31  46581  fourierdlem36  46586  fourierdlem37  46587  fourierdlem42  46592  fourierdlem79  46628  ioorrnopnlem  46747  hoicvr  46991  hoidmvlelem2  47039  iunhoiioolem  47118  vonioolem1  47123  fsupdm2  47286  finfdm2  47290  chnsuslle  47326  prmdvdsfmtnof1lem1  48062  prmdvdsfmtnof  48064  prmdvdsfmtnof1  48065  ssnn0ssfz  48840  rrx2plordso  49215