Theorem ltso 11370

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

Syntax hints:   Or wor 5606  ℝcr 11183   < clt 11324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-pre-lttri 11258  ax-pre-lttrn 11259

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329

This theorem is referenced by:  gtso  11371  lttri2  11372  lttri3  11373  lttri4  11374  ltnr  11385  ltnsym2  11389  fimaxre  12239  fiminre  12242  lbinf  12248  suprcl  12255  suprub  12256  suprlub  12259  infrecl  12277  infregelb  12279  infrelb  12280  supfirege  12282  suprfinzcl  12757  uzinfi  12993  suprzcl2  13003  suprzub  13004  2resupmax  13250  infmrp1  13406  fseqsupcl  14028  ssnn0fi  14036  fsuppmapnn0fiublem  14041  isercolllem1  15713  isercolllem2  15714  summolem2  15764  zsum  15766  fsumcvg3  15777  mertenslem2  15933  prodmolem2  15983  zprod  15985  cnso  16295  gcdval  16542  dfgcd2  16593  lcmval  16639  lcmgcdlem  16653  odzval  16838  pczpre  16894  prmreclem1  16963  ramz  17072  odval  19576  odf  19579  gexval  19620  gsumval3  19949  retos  21659  mbfsup  25718  mbfinf  25719  itg2monolem1  25805  itg2mono  25808  dvgt0lem2  26062  dvgt0  26063  plyeq0lem  26269  dgrval  26287  dgrcl  26292  dgrub  26293  dgrlb  26295  elqaalem1  26379  elqaalem3  26381  aalioulem2  26393  logccv  26723  ex-po  30467  ssnnssfz  32792  lmdvg  33899  oddpwdc  34319  ballotlemi  34465  ballotlemiex  34466  ballotlemsup  34469  ballotlemimin  34470  ballotlemfrcn0  34494  ballotlemirc  34496  erdszelem3  35161  erdszelem4  35162  erdszelem5  35163  erdszelem6  35164  erdszelem8  35166  erdszelem9  35167  erdszelem11  35169  erdsze2lem1  35171  erdsze2lem2  35172  supfz  35691  inffz  35692  gtinf  36285  ptrecube  37580  poimirlem31  37611  poimirlem32  37612  heicant  37615  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  incsequz2  37709  totbndbnd  37749  prdsbnd  37753  aks4d1p4  42036  aks4d1p7  42040  sticksstones1  42103  sticksstones3  42105  sn-suprcld  42449  sn-suprubd  42450  pellfundval  42836  dgraaval  43101  dgraaf  43104  fzisoeu  45215  uzublem  45345  infrglb  45511  limsupubuzlem  45633  fourierdlem25  46053  fourierdlem31  46059  fourierdlem36  46064  fourierdlem37  46065  fourierdlem42  46070  fourierdlem79  46106  ioorrnopnlem  46225  hoicvr  46469  hoidmvlelem2  46517  iunhoiioolem  46596  vonioolem1  46601  fsupdm2  46764  finfdm2  46768  prmdvdsfmtnof1lem1  47458  prmdvdsfmtnof  47460  prmdvdsfmtnof1  47461  ssnn0ssfz  48074  rrx2plordso  48458