Theorem ltso 10723

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

Syntax hints:   Or wor 5475  ℝcr 10538   < clt 10677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-pre-lttri 10613  ax-pre-lttrn 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-po 5476  df-so 5477  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-ltxr 10682

This theorem is referenced by:  gtso  10724  lttri2  10725  lttri3  10726  lttri4  10727  ltnr  10737  ltnsym2  10741  fimaxre  11586  fimaxreOLD  11587  fiminre  11590  lbinf  11596  suprcl  11603  suprub  11604  suprlub  11607  infrecl  11625  infregelb  11627  infrelb  11628  supfirege  11629  suprfinzcl  12100  uzinfi  12331  suprzcl2  12341  suprzub  12342  2resupmax  12584  infmrp1  12740  fseqsupcl  13348  ssnn0fi  13356  fsuppmapnn0fiublem  13361  isercolllem1  15023  isercolllem2  15024  summolem2  15075  zsum  15077  fsumcvg3  15088  mertenslem2  15243  prodmolem2  15291  zprod  15293  cnso  15602  gcdval  15847  dfgcd2  15896  lcmval  15938  lcmgcdlem  15952  odzval  16130  pczpre  16186  prmreclem1  16254  ramz  16363  odval  18664  odf  18667  gexval  18705  gsumval3  19029  retos  20764  mbfsup  24267  mbfinf  24268  itg2monolem1  24353  itg2mono  24356  dvgt0lem2  24602  dvgt0  24603  plyeq0lem  24802  dgrval  24820  dgrcl  24825  dgrub  24826  dgrlb  24828  elqaalem1  24910  elqaalem3  24912  aalioulem2  24924  logccv  25248  ex-po  28216  ssnnssfz  30512  lmdvg  31198  oddpwdc  31614  ballotlemi  31760  ballotlemiex  31761  ballotlemsup  31764  ballotlemimin  31765  ballotlemfrcn0  31789  ballotlemirc  31791  erdszelem3  32442  erdszelem4  32443  erdszelem5  32444  erdszelem6  32445  erdszelem8  32447  erdszelem9  32448  erdszelem11  32450  erdsze2lem1  32452  erdsze2lem2  32453  supfz  32962  inffz  32963  gtinf  33669  ptrecube  34894  poimirlem31  34925  poimirlem32  34926  heicant  34929  mblfinlem3  34933  mblfinlem4  34934  ismblfin  34935  incsequz2  35026  totbndbnd  35069  prdsbnd  35073  pellfundval  39484  dgraaval  39751  dgraaf  39754  fzisoeu  41574  uzublem  41711  infrglb  41878  limsupubuzlem  42000  fourierdlem25  42424  fourierdlem31  42430  fourierdlem36  42435  fourierdlem37  42436  fourierdlem42  42441  fourierdlem79  42477  ioorrnopnlem  42596  hoicvr  42837  hoidmvlelem2  42885  iunhoiioolem  42964  vonioolem1  42969  prmdvdsfmtnof1lem1  43753  prmdvdsfmtnof  43755  prmdvdsfmtnof1  43756  ssnn0ssfz  44404  rrx2plordso  44718