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 5569	1 ⊢ < Or ℝ

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-pre-lttri 11103  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  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  21608  mbfsup  25641  mbfinf  25642  itg2monolem1  25727  itg2mono  25730  dvgt0lem2  25980  dvgt0  25981  plyeq0lem  26185  dgrval  26203  dgrcl  26208  dgrub  26209  dgrlb  26211  elqaalem1  26296  elqaalem3  26298  aalioulem2  26310  logccv  26640  ex-po  30520  ssnnssfz  32875  lmdvg  34113  oddpwdc  34514  ballotlemi  34661  ballotlemiex  34662  ballotlemsup  34665  ballotlemimin  34666  ballotlemfrcn0  34690  ballotlemirc  34692  erdszelem3  35391  erdszelem4  35392  erdszelem5  35393  erdszelem6  35394  erdszelem8  35396  erdszelem9  35397  erdszelem11  35399  erdsze2lem1  35401  erdsze2lem2  35402  supfz  35927  inffz  35928  gtinf  36517  ptrecube  37955  poimirlem31  37986  poimirlem32  37987  heicant  37990  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  incsequz2  38084  totbndbnd  38124  prdsbnd  38128  aks4d1p4  42532  aks4d1p7  42536  sticksstones1  42599  sticksstones3  42601  sn-suprcld  42952  sn-suprubd  42953  pellfundval  43326  dgraaval  43590  dgraaf  43593  fzisoeu  45751  uzublem  45876  infrglb  46038  limsupubuzlem  46158  fourierdlem25  46578  fourierdlem31  46584  fourierdlem36  46589  fourierdlem37  46590  fourierdlem42  46595  fourierdlem79  46631  ioorrnopnlem  46750  hoicvr  46994  hoidmvlelem2  47042  iunhoiioolem  47121  vonioolem1  47126  fsupdm2  47289  finfdm2  47293  chnsuslle  47327  prmdvdsfmtnof1lem1  48059  prmdvdsfmtnof  48061  prmdvdsfmtnof1  48062  ssnn0ssfz  48837  rrx2plordso  49212