Theorem ltso 11338

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

Syntax hints:   Or wor 5595  ℝcr 11151   < clt 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-pre-lttri 11226  ax-pre-lttrn 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297

This theorem is referenced by:  gtso  11339  lttri2  11340  lttri3  11341  lttri4  11342  ltnr  11353  ltnsym2  11357  fimaxre  12209  fiminre  12212  lbinf  12218  suprcl  12225  suprub  12226  suprlub  12229  infrecl  12247  infregelb  12249  infrelb  12250  supfirege  12252  suprfinzcl  12729  uzinfi  12967  suprzcl2  12977  suprzub  12978  2resupmax  13226  infmrp1  13382  fseqsupcl  14014  ssnn0fi  14022  fsuppmapnn0fiublem  14027  isercolllem1  15697  isercolllem2  15698  summolem2  15748  zsum  15750  fsumcvg3  15761  mertenslem2  15917  prodmolem2  15967  zprod  15969  cnso  16279  gcdval  16529  dfgcd2  16579  lcmval  16625  lcmgcdlem  16639  odzval  16824  pczpre  16880  prmreclem1  16949  ramz  17058  odval  19566  odf  19569  gexval  19610  gsumval3  19939  retos  21653  mbfsup  25712  mbfinf  25713  itg2monolem1  25799  itg2mono  25802  dvgt0lem2  26056  dvgt0  26057  plyeq0lem  26263  dgrval  26281  dgrcl  26286  dgrub  26287  dgrlb  26289  elqaalem1  26375  elqaalem3  26377  aalioulem2  26389  logccv  26719  ex-po  30463  ssnnssfz  32795  lmdvg  33913  oddpwdc  34335  ballotlemi  34481  ballotlemiex  34482  ballotlemsup  34485  ballotlemimin  34486  ballotlemfrcn0  34510  ballotlemirc  34512  erdszelem3  35177  erdszelem4  35178  erdszelem5  35179  erdszelem6  35180  erdszelem8  35182  erdszelem9  35183  erdszelem11  35185  erdsze2lem1  35187  erdsze2lem2  35188  supfz  35708  inffz  35709  gtinf  36301  ptrecube  37606  poimirlem31  37637  poimirlem32  37638  heicant  37641  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  incsequz2  37735  totbndbnd  37775  prdsbnd  37779  aks4d1p4  42060  aks4d1p7  42064  sticksstones1  42127  sticksstones3  42129  sn-suprcld  42479  sn-suprubd  42480  pellfundval  42867  dgraaval  43132  dgraaf  43135  fzisoeu  45250  uzublem  45379  infrglb  45545  limsupubuzlem  45667  fourierdlem25  46087  fourierdlem31  46093  fourierdlem36  46098  fourierdlem37  46099  fourierdlem42  46104  fourierdlem79  46140  ioorrnopnlem  46259  hoicvr  46503  hoidmvlelem2  46551  iunhoiioolem  46630  vonioolem1  46635  fsupdm2  46798  finfdm2  46802  prmdvdsfmtnof1lem1  47508  prmdvdsfmtnof  47510  prmdvdsfmtnof1  47511  ssnn0ssfz  48193  rrx2plordso  48573