Theorem ltso 11261

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

Syntax hints:   Or wor 5548  ℝcr 11074   < clt 11215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-pre-lttri 11149  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220

This theorem is referenced by:  gtso  11262  lttri2  11263  lttri3  11264  lttri4  11265  ltnr  11276  ltnsym2  11280  fimaxre  12134  fiminre  12137  lbinf  12143  suprcl  12150  suprub  12151  suprlub  12154  infrecl  12172  infregelb  12174  infrelb  12175  supfirege  12177  suprfinzcl  12655  uzinfi  12894  suprzcl2  12904  suprzub  12905  2resupmax  13155  infmrp1  13312  fseqsupcl  13949  ssnn0fi  13957  fsuppmapnn0fiublem  13962  isercolllem1  15638  isercolllem2  15639  summolem2  15689  zsum  15691  fsumcvg3  15702  mertenslem2  15858  prodmolem2  15908  zprod  15910  cnso  16222  gcdval  16473  dfgcd2  16523  lcmval  16569  lcmgcdlem  16583  odzval  16769  pczpre  16825  prmreclem1  16894  ramz  17003  odval  19471  odf  19474  gexval  19515  gsumval3  19844  retos  21534  mbfsup  25572  mbfinf  25573  itg2monolem1  25658  itg2mono  25661  dvgt0lem2  25915  dvgt0  25916  plyeq0lem  26122  dgrval  26140  dgrcl  26145  dgrub  26146  dgrlb  26148  elqaalem1  26234  elqaalem3  26236  aalioulem2  26248  logccv  26579  ex-po  30371  ssnnssfz  32717  lmdvg  33950  oddpwdc  34352  ballotlemi  34499  ballotlemiex  34500  ballotlemsup  34503  ballotlemimin  34504  ballotlemfrcn0  34528  ballotlemirc  34530  erdszelem3  35187  erdszelem4  35188  erdszelem5  35189  erdszelem6  35190  erdszelem8  35192  erdszelem9  35193  erdszelem11  35195  erdsze2lem1  35197  erdsze2lem2  35198  supfz  35723  inffz  35724  gtinf  36314  ptrecube  37621  poimirlem31  37652  poimirlem32  37653  heicant  37656  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  incsequz2  37750  totbndbnd  37790  prdsbnd  37794  aks4d1p4  42074  aks4d1p7  42078  sticksstones1  42141  sticksstones3  42143  sn-suprcld  42488  sn-suprubd  42489  pellfundval  42875  dgraaval  43140  dgraaf  43143  fzisoeu  45305  uzublem  45433  infrglb  45595  limsupubuzlem  45717  fourierdlem25  46137  fourierdlem31  46143  fourierdlem36  46148  fourierdlem37  46149  fourierdlem42  46154  fourierdlem79  46190  ioorrnopnlem  46309  hoicvr  46553  hoidmvlelem2  46601  iunhoiioolem  46680  vonioolem1  46685  fsupdm2  46848  finfdm2  46852  prmdvdsfmtnof1lem1  47589  prmdvdsfmtnof  47591  prmdvdsfmtnof1  47592  ssnn0ssfz  48341  rrx2plordso  48717