Theorem ltso 10457

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

Syntax hints:   Or wor 5273  ℝcr 10271   < clt 10411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-pre-lttri 10346  ax-pre-lttrn 10347

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-ltxr 10416

This theorem is referenced by:  gtso  10458  lttri2  10459  lttri3  10460  lttri4  10461  ltnr  10471  ltnsym2  10475  fimaxre  11322  lbinf  11330  suprcl  11337  suprub  11338  suprlub  11341  infrecl  11359  infregelb  11361  infrelb  11362  supfirege  11363  suprfinzcl  11844  uzinfi  12075  suprzcl2  12085  suprzub  12086  2resupmax  12331  infmrp1  12486  fseqsupcl  13095  ssnn0fi  13103  fsuppmapnn0fiublem  13108  isercolllem1  14803  isercolllem2  14804  summolem2  14854  zsum  14856  fsumcvg3  14867  mertenslem2  15020  prodmolem2  15068  zprod  15070  cnso  15380  gcdval  15624  dfgcd2  15669  lcmval  15711  lcmgcdlem  15725  odzval  15900  pczpre  15956  prmreclem1  16024  ramz  16133  odval  18337  odf  18340  gexval  18377  gsumval3  18694  retos  20361  mbfsup  23868  mbfinf  23869  itg2monolem1  23954  itg2mono  23957  dvgt0lem2  24203  dvgt0  24204  plyeq0lem  24403  dgrval  24421  dgrcl  24426  dgrub  24427  dgrlb  24429  elqaalem1  24511  elqaalem3  24513  aalioulem2  24525  logccv  24846  ex-po  27867  ssnnssfz  30113  lmdvg  30597  oddpwdc  31014  ballotlemi  31161  ballotlemiex  31162  ballotlemsup  31165  ballotlemimin  31166  ballotlemfrcn0  31190  ballotlemirc  31192  erdszelem3  31774  erdszelem4  31775  erdszelem5  31776  erdszelem6  31777  erdszelem8  31779  erdszelem9  31780  erdszelem11  31782  erdsze2lem1  31784  erdsze2lem2  31785  supfz  32208  inffz  32209  gtinf  32902  ptrecube  34030  poimirlem31  34061  poimirlem32  34062  heicant  34065  mblfinlem3  34069  mblfinlem4  34070  ismblfin  34071  incsequz2  34164  totbndbnd  34207  prdsbnd  34211  pellfundval  38397  dgraaval  38666  dgraaf  38669  fzisoeu  40416  uzublem  40556  infrglb  40723  limsupubuzlem  40845  fourierdlem25  41269  fourierdlem31  41275  fourierdlem36  41280  fourierdlem37  41281  fourierdlem42  41286  fourierdlem79  41322  ioorrnopnlem  41441  hoicvr  41682  hoidmvlelem2  41730  iunhoiioolem  41809  vonioolem1  41814  prmdvdsfmtnof1lem1  42510  prmdvdsfmtnof  42512  prmdvdsfmtnof1  42513  ssnn0ssfz  43135  rrx2plordso  43453