Theorem ltso 11290

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

Syntax hints:   Or wor 5569  ℝcr 11099   < clt 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11157  ax-pre-lttri 11174  ax-pre-lttrn 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-ltxr 11248

This theorem is referenced by:  gtso  11291  lttri2  11292  lttri3  11293  lttri4  11294  ltnr  11305  ltnsym2  11309  fimaxre  12159  fiminre  12162  lbinf  12168  suprcl  12175  suprub  12176  suprlub  12179  infrecl  12197  infregelb  12199  infrelb  12200  supfirege  12202  suprfinzcl  12710  uzinfi  12952  suprzcl2  12962  suprzub  12963  2resupmax  13214  infmrp1  13371  fseqsupcl  14013  ssnn0fi  14021  fsuppmapnn0fiublem  14026  isercolllem1  15716  isercolllem2  15717  summolem2  15767  zsum  15769  fsumcvg3  15780  mertenslem2  15939  prodmolem2  15989  zprod  15991  cnso  16303  gcdval  16554  dfgcd2  16604  lcmval  16650  lcmgcdlem  16664  odzval  16851  pczpre  16907  prmreclem1  16976  ramz  17085  odval  19604  odf  19607  gexval  19648  gsumval3  19977  retos  21737  mbfsup  25792  mbfinf  25793  itg2monolem1  25878  itg2mono  25881  dvgt0lem2  26131  dvgt0  26132  plyeq0lem  26336  dgrval  26354  dgrcl  26359  dgrub  26360  dgrlb  26362  elqaalem1  26449  elqaalem3  26451  aalioulem2  26463  logccv  26794  ex-po  30727  ssnnssfz  33073  lmdvg  34288  oddpwdc  34689  ballotlemi  34836  ballotlemiex  34837  ballotlemsup  34840  ballotlemimin  34841  ballotlemfrcn0  34865  ballotlemirc  34867  erdszelem3  35618  erdszelem4  35619  erdszelem5  35620  erdszelem6  35621  erdszelem8  35623  erdszelem9  35624  erdszelem11  35626  erdsze2lem1  35628  erdsze2lem2  35629  supfz  36154  inffz  36155  gtinf  36753  ptrecube  38193  poimirlem31  38224  poimirlem32  38225  heicant  38228  mblfinlem3  38232  mblfinlem4  38233  ismblfin  38234  incsequz2  38322  totbndbnd  38362  prdsbnd  38366  aks4d1p4  42770  aks4d1p7  42774  sticksstones1  42837  sticksstones3  42839  sn-suprcld  43191  sn-suprubd  43192  pellfundval  43533  dgraaval  43797  dgraaf  43800  fzisoeu  45945  uzublem  46070  infrglb  46232  limsupubuzlem  46352  fourierdlem25  46772  fourierdlem31  46778  fourierdlem36  46783  fourierdlem37  46784  fourierdlem42  46789  fourierdlem79  46825  ioorrnopnlem  46944  hoicvr  47188  hoidmvlelem2  47236  iunhoiioolem  47315  vonioolem1  47320  fsupdm2  47483  finfdm2  47487  chnsuslle  47523  prmdvdsfmtnof1lem1  48259  prmdvdsfmtnof  48261  prmdvdsfmtnof1  48262  ssnn0ssfz  49048  rrx2plordso  49423