Theorem ltso 11193

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

Syntax hints:   Or wor 5521  ℝcr 11005   < clt 11146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-pre-lttri 11080  ax-pre-lttrn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-ltxr 11151

This theorem is referenced by:  gtso  11194  lttri2  11195  lttri3  11196  lttri4  11197  ltnr  11208  ltnsym2  11212  fimaxre  12066  fiminre  12069  lbinf  12075  suprcl  12082  suprub  12083  suprlub  12086  infrecl  12104  infregelb  12106  infrelb  12107  supfirege  12109  suprfinzcl  12587  uzinfi  12826  suprzcl2  12836  suprzub  12837  2resupmax  13087  infmrp1  13244  fseqsupcl  13884  ssnn0fi  13892  fsuppmapnn0fiublem  13897  isercolllem1  15572  isercolllem2  15573  summolem2  15623  zsum  15625  fsumcvg3  15636  mertenslem2  15792  prodmolem2  15842  zprod  15844  cnso  16156  gcdval  16407  dfgcd2  16457  lcmval  16503  lcmgcdlem  16517  odzval  16703  pczpre  16759  prmreclem1  16828  ramz  16937  odval  19446  odf  19449  gexval  19490  gsumval3  19819  retos  21555  mbfsup  25592  mbfinf  25593  itg2monolem1  25678  itg2mono  25681  dvgt0lem2  25935  dvgt0  25936  plyeq0lem  26142  dgrval  26160  dgrcl  26165  dgrub  26166  dgrlb  26168  elqaalem1  26254  elqaalem3  26256  aalioulem2  26268  logccv  26599  ex-po  30415  ssnnssfz  32770  lmdvg  33966  oddpwdc  34367  ballotlemi  34514  ballotlemiex  34515  ballotlemsup  34518  ballotlemimin  34519  ballotlemfrcn0  34543  ballotlemirc  34545  erdszelem3  35237  erdszelem4  35238  erdszelem5  35239  erdszelem6  35240  erdszelem8  35242  erdszelem9  35243  erdszelem11  35245  erdsze2lem1  35247  erdsze2lem2  35248  supfz  35773  inffz  35774  gtinf  36361  ptrecube  37668  poimirlem31  37699  poimirlem32  37700  heicant  37703  mblfinlem3  37707  mblfinlem4  37708  ismblfin  37709  incsequz2  37797  totbndbnd  37837  prdsbnd  37841  aks4d1p4  42120  aks4d1p7  42124  sticksstones1  42187  sticksstones3  42189  sn-suprcld  42534  sn-suprubd  42535  pellfundval  42921  dgraaval  43185  dgraaf  43188  fzisoeu  45349  uzublem  45476  infrglb  45638  limsupubuzlem  45758  fourierdlem25  46178  fourierdlem31  46184  fourierdlem36  46189  fourierdlem37  46190  fourierdlem42  46195  fourierdlem79  46231  ioorrnopnlem  46350  hoicvr  46594  hoidmvlelem2  46642  iunhoiioolem  46721  vonioolem1  46726  fsupdm2  46889  finfdm2  46893  prmdvdsfmtnof1lem1  47623  prmdvdsfmtnof  47625  prmdvdsfmtnof1  47626  ssnn0ssfz  48388  rrx2plordso  48764