Theorem ltso 11254

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

Syntax hints:   Or wor 5545  ℝcr 11067   < clt 11208

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 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-pre-lttri 11142  ax-pre-lttrn 11143

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213

This theorem is referenced by:  gtso  11255  lttri2  11256  lttri3  11257  lttri4  11258  ltnr  11269  ltnsym2  11273  fimaxre  12127  fiminre  12130  lbinf  12136  suprcl  12143  suprub  12144  suprlub  12147  infrecl  12165  infregelb  12167  infrelb  12168  supfirege  12170  suprfinzcl  12648  uzinfi  12887  suprzcl2  12897  suprzub  12898  2resupmax  13148  infmrp1  13305  fseqsupcl  13942  ssnn0fi  13950  fsuppmapnn0fiublem  13955  isercolllem1  15631  isercolllem2  15632  summolem2  15682  zsum  15684  fsumcvg3  15695  mertenslem2  15851  prodmolem2  15901  zprod  15903  cnso  16215  gcdval  16466  dfgcd2  16516  lcmval  16562  lcmgcdlem  16576  odzval  16762  pczpre  16818  prmreclem1  16887  ramz  16996  odval  19464  odf  19467  gexval  19508  gsumval3  19837  retos  21527  mbfsup  25565  mbfinf  25566  itg2monolem1  25651  itg2mono  25654  dvgt0lem2  25908  dvgt0  25909  plyeq0lem  26115  dgrval  26133  dgrcl  26138  dgrub  26139  dgrlb  26141  elqaalem1  26227  elqaalem3  26229  aalioulem2  26241  logccv  26572  ex-po  30364  ssnnssfz  32710  lmdvg  33943  oddpwdc  34345  ballotlemi  34492  ballotlemiex  34493  ballotlemsup  34496  ballotlemimin  34497  ballotlemfrcn0  34521  ballotlemirc  34523  erdszelem3  35180  erdszelem4  35181  erdszelem5  35182  erdszelem6  35183  erdszelem8  35185  erdszelem9  35186  erdszelem11  35188  erdsze2lem1  35190  erdsze2lem2  35191  supfz  35716  inffz  35717  gtinf  36307  ptrecube  37614  poimirlem31  37645  poimirlem32  37646  heicant  37649  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  incsequz2  37743  totbndbnd  37783  prdsbnd  37787  aks4d1p4  42067  aks4d1p7  42071  sticksstones1  42134  sticksstones3  42136  sn-suprcld  42481  sn-suprubd  42482  pellfundval  42868  dgraaval  43133  dgraaf  43136  fzisoeu  45298  uzublem  45426  infrglb  45588  limsupubuzlem  45710  fourierdlem25  46130  fourierdlem31  46136  fourierdlem36  46141  fourierdlem37  46142  fourierdlem42  46147  fourierdlem79  46183  ioorrnopnlem  46302  hoicvr  46546  hoidmvlelem2  46594  iunhoiioolem  46673  vonioolem1  46678  fsupdm2  46841  finfdm2  46845  prmdvdsfmtnof1lem1  47585  prmdvdsfmtnof  47587  prmdvdsfmtnof1  47588  ssnn0ssfz  48337  rrx2plordso  48713