Theorem ltso 11064

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

Syntax hints:   Or wor 5503  ℝcr 10879   < clt 11018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-pre-lttri 10954  ax-pre-lttrn 10955

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-ltxr 11023

This theorem is referenced by:  gtso  11065  lttri2  11066  lttri3  11067  lttri4  11068  ltnr  11079  ltnsym2  11083  fimaxre  11928  fiminre  11931  lbinf  11937  suprcl  11944  suprub  11945  suprlub  11948  infrecl  11966  infregelb  11968  infrelb  11969  supfirege  11971  suprfinzcl  12445  uzinfi  12677  suprzcl2  12687  suprzub  12688  2resupmax  12931  infmrp1  13087  fseqsupcl  13706  ssnn0fi  13714  fsuppmapnn0fiublem  13719  isercolllem1  15385  isercolllem2  15386  summolem2  15437  zsum  15439  fsumcvg3  15450  mertenslem2  15606  prodmolem2  15654  zprod  15656  cnso  15965  gcdval  16212  dfgcd2  16263  lcmval  16306  lcmgcdlem  16320  odzval  16501  pczpre  16557  prmreclem1  16626  ramz  16735  odval  19151  odf  19154  gexval  19192  gsumval3  19517  retos  20832  mbfsup  24837  mbfinf  24838  itg2monolem1  24924  itg2mono  24927  dvgt0lem2  25176  dvgt0  25177  plyeq0lem  25380  dgrval  25398  dgrcl  25403  dgrub  25404  dgrlb  25406  elqaalem1  25488  elqaalem3  25490  aalioulem2  25502  logccv  25827  ex-po  28808  ssnnssfz  31117  lmdvg  31912  oddpwdc  32330  ballotlemi  32476  ballotlemiex  32477  ballotlemsup  32480  ballotlemimin  32481  ballotlemfrcn0  32505  ballotlemirc  32507  erdszelem3  33164  erdszelem4  33165  erdszelem5  33166  erdszelem6  33167  erdszelem8  33169  erdszelem9  33170  erdszelem11  33172  erdsze2lem1  33174  erdsze2lem2  33175  supfz  33703  inffz  33704  gtinf  34517  ptrecube  35786  poimirlem31  35817  poimirlem32  35818  heicant  35821  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  incsequz2  35916  totbndbnd  35956  prdsbnd  35960  aks4d1p4  40094  aks4d1p7  40098  sticksstones1  40109  sticksstones3  40111  pellfundval  40709  dgraaval  40976  dgraaf  40979  fzisoeu  42846  uzublem  42977  infrglb  43138  limsupubuzlem  43260  fourierdlem25  43680  fourierdlem31  43686  fourierdlem36  43691  fourierdlem37  43692  fourierdlem42  43697  fourierdlem79  43733  ioorrnopnlem  43852  hoicvr  44093  hoidmvlelem2  44141  iunhoiioolem  44220  vonioolem1  44225  prmdvdsfmtnof1lem1  45047  prmdvdsfmtnof  45049  prmdvdsfmtnof1  45050  ssnn0ssfz  45696  rrx2plordso  46081