Theorem ltso 11257

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

Syntax hints:   Or wor 5550  ℝcr 11066   < clt 11210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-pre-lttri 11141  ax-pre-lttrn 11142

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-ltxr 11215

This theorem is referenced by:  gtso  11258  lttri2  11259  lttri3  11260  lttri4  11261  ltnr  11272  ltnsym2  11276  fimaxre  12130  fiminre  12133  lbinf  12139  suprcl  12146  suprub  12147  suprlub  12150  infrecl  12168  infregelb  12170  infrelb  12171  supfirege  12173  suprfinzcl  12681  uzinfi  12923  suprzcl2  12933  suprzub  12934  2resupmax  13185  infmrp1  13342  fseqsupcl  13984  ssnn0fi  13992  fsuppmapnn0fiublem  13997  isercolllem1  15683  isercolllem2  15684  summolem2  15734  zsum  15736  fsumcvg3  15747  mertenslem2  15906  prodmolem2  15956  zprod  15958  cnso  16270  gcdval  16521  dfgcd2  16571  lcmval  16617  lcmgcdlem  16631  odzval  16818  pczpre  16874  prmreclem1  16943  ramz  17052  odval  19565  odf  19568  gexval  19609  gsumval3  19938  retos  21658  mbfsup  25714  mbfinf  25715  itg2monolem1  25800  itg2mono  25803  dvgt0lem2  26053  dvgt0  26054  plyeq0lem  26258  dgrval  26276  dgrcl  26281  dgrub  26282  dgrlb  26284  elqaalem1  26371  elqaalem3  26373  aalioulem2  26385  logccv  26716  ex-po  30594  ssnnssfz  32950  lmdvg  34211  oddpwdc  34612  ballotlemi  34759  ballotlemiex  34760  ballotlemsup  34763  ballotlemimin  34764  ballotlemfrcn0  34788  ballotlemirc  34790  erdszelem3  35504  erdszelem4  35505  erdszelem5  35506  erdszelem6  35507  erdszelem8  35509  erdszelem9  35510  erdszelem11  35512  erdsze2lem1  35514  erdsze2lem2  35515  supfz  36040  inffz  36041  gtinf  36640  ptrecube  38080  poimirlem31  38111  poimirlem32  38112  heicant  38115  mblfinlem3  38119  mblfinlem4  38120  ismblfin  38121  incsequz2  38209  totbndbnd  38249  prdsbnd  38253  aks4d1p4  42657  aks4d1p7  42661  sticksstones1  42724  sticksstones3  42726  sn-suprcld  43076  sn-suprubd  43077  pellfundval  43418  dgraaval  43682  dgraaf  43685  fzisoeu  45840  uzublem  45965  infrglb  46127  limsupubuzlem  46247  fourierdlem25  46667  fourierdlem31  46673  fourierdlem36  46678  fourierdlem37  46679  fourierdlem42  46684  fourierdlem79  46720  ioorrnopnlem  46839  hoicvr  47083  hoidmvlelem2  47131  iunhoiioolem  47210  vonioolem1  47215  fsupdm2  47378  finfdm2  47382  chnsuslle  47418  prmdvdsfmtnof1lem1  48154  prmdvdsfmtnof  48156  prmdvdsfmtnof1  48157  ssnn0ssfz  48932  rrx2plordso  49307