Theorem ltso 11285

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

Syntax hints:   Or wor 5568  ℝcr 11094   < clt 11238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-pre-lttri 11169  ax-pre-lttrn 11170

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-ltxr 11243

This theorem is referenced by:  gtso  11286  lttri2  11287  lttri3  11288  lttri4  11289  ltnr  11300  ltnsym2  11304  fimaxre  12154  fiminre  12157  lbinf  12163  suprcl  12170  suprub  12171  suprlub  12174  infrecl  12192  infregelb  12194  infrelb  12195  supfirege  12197  suprfinzcl  12705  uzinfi  12947  suprzcl2  12957  suprzub  12958  2resupmax  13209  infmrp1  13366  fseqsupcl  14009  ssnn0fi  14017  fsuppmapnn0fiublem  14022  isercolllem1  15712  isercolllem2  15713  summolem2  15763  zsum  15765  fsumcvg3  15776  mertenslem2  15935  prodmolem2  15985  zprod  15987  cnso  16298  gcdval  16549  dfgcd2  16599  lcmval  16645  lcmgcdlem  16659  odzval  16846  pczpre  16902  prmreclem1  16971  ramz  17080  odval  19599  odf  19602  gexval  19643  gsumval3  19972  retos  21768  mbfsup  25823  mbfinf  25824  itg2monolem1  25909  itg2mono  25912  dvgt0lem2  26162  dvgt0  26163  plyeq0lem  26367  dgrval  26385  dgrcl  26390  dgrub  26391  dgrlb  26393  elqaalem1  26480  elqaalem3  26482  aalioulem2  26496  logccv  26828  ex-po  30786  ssnnssfz  33132  lmdvg  34343  oddpwdc  34744  ballotlemi  34891  ballotlemiex  34892  ballotlemsup  34895  ballotlemimin  34896  ballotlemfrcn0  34920  ballotlemirc  34922  erdszelem3  35685  erdszelem4  35686  erdszelem5  35687  erdszelem6  35688  erdszelem8  35690  erdszelem9  35691  erdszelem11  35693  erdsze2lem1  35695  erdsze2lem2  35696  supfz  36221  inffz  36222  gtinf  36830  ptrecube  38271  poimirlem31  38302  poimirlem32  38303  heicant  38306  mblfinlem3  38310  mblfinlem4  38311  ismblfin  38312  incsequz2  38400  totbndbnd  38440  prdsbnd  38444  aks4d1p4  42846  aks4d1p7  42850  sticksstones1  42913  sticksstones3  42915  sn-suprcld  43267  sn-suprubd  43268  pellfundval  43607  dgraaval  43871  dgraaf  43874  fzisoeu  46019  uzublem  46144  infrglb  46306  limsupubuzlem  46426  fourierdlem25  46846  fourierdlem31  46852  fourierdlem36  46857  fourierdlem37  46858  fourierdlem42  46863  fourierdlem79  46899  ioorrnopnlem  47018  hoicvr  47262  hoidmvlelem2  47310  iunhoiioolem  47389  vonioolem1  47394  fsupdm2  47557  finfdm2  47561  chnsuslle  47597  prmdvdsfmtnof1lem1  48336  prmdvdsfmtnof  48338  prmdvdsfmtnof1  48339  ssnn0ssfz  49129  rrx2plordso  49504