Theorem ltso 11397

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

This proof depends on syntax axioms:   Or wor 5558  ℝcr 11206   < clt 11350

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-resscn 11264  ax-pre-lttri 11281  ax-pre-lttrn 11282

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8724  df-en 8981  df-dom 8982  df-sdom 8983  df-pnf 11352  df-mnf 11353  df-ltxr 11355

This theorem is used by:  gtso  11398  lttri2  11399  lttri3  11400  lttri4  11401  ltnr  11412  ltnsym2  11416  fimaxre  12268  fiminre  12271  lbinf  12277  suprcl  12284  suprub  12285  suprlub  12288  infrecl  12306  infregelb  12308  infrelb  12309  supfirege  12311  suprfinzcl  12820  uzinfi  13062  suprzcl2  13072  suprzub  13073  2resupmax  13325  infmrp1  13482  fseqsupcl  14127  ssnn0fi  14135  fsuppmapnn0fiublem  14140  isercolllem1  15841  isercolllem2  15842  summolem2  15891  zsum  15893  fsumcvg3  15904  mertenslem2  16063  prodmolem2  16111  zprod  16113  cnso  16424  gcdval  16675  dfgcd2  16728  lcmval  16776  lcmgcdlem  16790  odzval  16978  pczpre  17034  prmreclem1  17103  ramz  17212  odval  19757  odf  19760  gexval  19801  gsumval3  20130  retos  21933  mbfsup  25994  mbfinf  25995  itg2monolem1  26080  itg2mono  26083  dvgt0lem2  26332  dvgt0  26333  plyeq0lem  26538  dgrval  26556  dgrcl  26561  dgrub  26562  dgrlb  26564  elqaalem1  26651  elqaalem3  26653  aalioulem2  26669  logccv  27000  ex-po  31045  ssnnssfz  33429  lmdvg  34635  oddpwdc  35036  ballotlemi  35183  ballotlemiex  35184  ballotlemsup  35187  ballotlemimin  35188  ballotlemfrcn0  35212  ballotlemirc  35214  erdszelem3  36048  erdszelem4  36049  erdszelem5  36050  erdszelem6  36051  erdszelem8  36053  erdszelem9  36054  erdszelem11  36056  erdsze2lem1  36058  erdsze2lem2  36059  supfz  36590  inffz  36591  gtinf  37203  ptrecube  38647  poimirlem31  38678  poimirlem32  38679  heicant  38682  mblfinlem3  38686  mblfinlem4  38687  ismblfin  38688  incsequz2  38792  totbndbnd  38832  prdsbnd  38836  aks4d1p4  43238  aks4d1p7  43242  sticksstones1  43305  sticksstones3  43307  sn-suprcld  43666  sn-suprubd  43667  frlmnzcoordval  43762  frlmnzcoordcl  43764  frlmnzcoordn0  43766  pellfundval  43996  dgraaval  44255  dgraaf  44258  fzisoeu  46424  uzublem  46548  infrglb  46710  limsupubuzlem  46830  fourierdlem25  47250  fourierdlem31  47256  fourierdlem36  47261  fourierdlem37  47262  fourierdlem42  47267  fourierdlem79  47303  ioorrnopnlem  47422  hoicvr  47666  hoidmvlelem2  47714  iunhoiioolem  47793  vonioolem1  47798  fsupdm2  47961  finfdm2  47965  chnsuslle  47999  prmdvdsfmtnof1lem1  48777  prmdvdsfmtnof  48779  prmdvdsfmtnof1  48780  ssnn0ssfz  49569  rrx2plordso  49945