Theorem ltso 10306

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

Syntax hints:   Or wor 5182  ℝcr 10123   < clt 10262

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-resscn 10181  ax-pre-lttri 10198  ax-pre-lttrn 10199

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-po 5183  df-so 5184  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-er 7907  df-en 8118  df-dom 8119  df-sdom 8120  df-pnf 10264  df-mnf 10265  df-ltxr 10267

This theorem is referenced by:  gtso  10307  lttri2  10308  lttri3  10309  lttri4  10310  ltnr  10320  ltnsym2  10324  fimaxre  11156  lbinf  11164  suprcl  11171  suprub  11172  suprlub  11175  infrecl  11193  infregelb  11195  infrelb  11196  supfirege  11197  suprfinzcl  11680  uzinfi  11957  suprzcl2  11967  suprzub  11968  2resupmax  12208  infmrp1  12363  fseqsupcl  12966  ssnn0fi  12974  fsuppmapnn0fiublem  12979  isercolllem1  14590  isercolllem2  14591  summolem2  14642  zsum  14644  fsumcvg3  14655  mertenslem2  14812  prodmolem2  14860  zprod  14862  cnso  15171  gcdval  15416  dfgcd2  15461  lcmval  15503  lcmgcdlem  15517  odzval  15694  pczpre  15750  prmreclem1  15818  ramz  15927  odval  18149  odf  18152  gexval  18189  gsumval3  18504  retos  20162  mbfsup  23626  mbfinf  23627  itg2monolem1  23712  itg2mono  23715  dvgt0lem2  23961  dvgt0  23962  plyeq0lem  24161  dgrval  24179  dgrcl  24184  dgrub  24185  dgrlb  24187  elqaalem1  24269  elqaalem3  24271  aalioulem2  24283  logccv  24604  ex-po  27599  ssnnssfz  29854  lmdvg  30304  oddpwdc  30721  ballotlemi  30867  ballotlemiex  30868  ballotlemsup  30871  ballotlemimin  30872  ballotlemfrcn0  30896  ballotlemirc  30898  erdszelem3  31478  erdszelem4  31479  erdszelem5  31480  erdszelem6  31481  erdszelem8  31483  erdszelem9  31484  erdszelem11  31486  erdsze2lem1  31488  erdsze2lem2  31489  supfz  31916  inffz  31917  inffzOLD  31918  gtinf  32615  ptrecube  33718  poimirlem31  33749  poimirlem32  33750  heicant  33753  mblfinlem3  33757  mblfinlem4  33758  ismblfin  33759  incsequz2  33854  totbndbnd  33897  prdsbnd  33901  pellfundval  37942  dgraaval  38212  dgraaf  38215  fzisoeu  40009  uzublem  40151  infrglb  40321  limsupubuzlem  40443  fourierdlem25  40848  fourierdlem31  40854  fourierdlem36  40859  fourierdlem37  40860  fourierdlem42  40865  fourierdlem79  40901  ioorrnopnlem  41023  hoicvr  41264  hoidmvlelem2  41312  iunhoiioolem  41391  vonioolem1  41396  prmdvdsfmtnof1lem1  42002  prmdvdsfmtnof  42004  prmdvdsfmtnof1  42005  ssnn0ssfz  42633