Theorem ltso 10710

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

Syntax hints:   Or wor 5437  ℝcr 10525   < clt 10664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-pre-lttri 10600  ax-pre-lttrn 10601

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-ltxr 10669

This theorem is referenced by:  gtso  10711  lttri2  10712  lttri3  10713  lttri4  10714  ltnr  10724  ltnsym2  10728  fimaxre  11573  fiminre  11576  lbinf  11581  suprcl  11588  suprub  11589  suprlub  11592  infrecl  11610  infregelb  11612  infrelb  11613  supfirege  11614  suprfinzcl  12085  uzinfi  12316  suprzcl2  12326  suprzub  12327  2resupmax  12569  infmrp1  12725  fseqsupcl  13340  ssnn0fi  13348  fsuppmapnn0fiublem  13353  isercolllem1  15013  isercolllem2  15014  summolem2  15065  zsum  15067  fsumcvg3  15078  mertenslem2  15233  prodmolem2  15281  zprod  15283  cnso  15592  gcdval  15835  dfgcd2  15884  lcmval  15926  lcmgcdlem  15940  odzval  16118  pczpre  16174  prmreclem1  16242  ramz  16351  odval  18654  odf  18657  gexval  18695  gsumval3  19020  retos  20307  mbfsup  24268  mbfinf  24269  itg2monolem1  24354  itg2mono  24357  dvgt0lem2  24606  dvgt0  24607  plyeq0lem  24807  dgrval  24825  dgrcl  24830  dgrub  24831  dgrlb  24833  elqaalem1  24915  elqaalem3  24917  aalioulem2  24929  logccv  25254  ex-po  28220  ssnnssfz  30536  lmdvg  31306  oddpwdc  31722  ballotlemi  31868  ballotlemiex  31869  ballotlemsup  31872  ballotlemimin  31873  ballotlemfrcn0  31897  ballotlemirc  31899  erdszelem3  32553  erdszelem4  32554  erdszelem5  32555  erdszelem6  32556  erdszelem8  32558  erdszelem9  32559  erdszelem11  32561  erdsze2lem1  32563  erdsze2lem2  32564  supfz  33073  inffz  33074  gtinf  33780  ptrecube  35057  poimirlem31  35088  poimirlem32  35089  heicant  35092  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  incsequz2  35187  totbndbnd  35227  prdsbnd  35231  pellfundval  39821  dgraaval  40088  dgraaf  40091  fzisoeu  41932  uzublem  42067  infrglb  42232  limsupubuzlem  42354  fourierdlem25  42774  fourierdlem31  42780  fourierdlem36  42785  fourierdlem37  42786  fourierdlem42  42791  fourierdlem79  42827  ioorrnopnlem  42946  hoicvr  43187  hoidmvlelem2  43235  iunhoiioolem  43314  vonioolem1  43319  prmdvdsfmtnof1lem1  44101  prmdvdsfmtnof  44103  prmdvdsfmtnof1  44104  ssnn0ssfz  44751  rrx2plordso  45138