Theorem ltso 11225

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

Syntax hints:   Or wor 5539  ℝcr 11037   < clt 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183

This theorem is referenced by:  gtso  11226  lttri2  11227  lttri3  11228  lttri4  11229  ltnr  11240  ltnsym2  11244  fimaxre  12098  fiminre  12101  lbinf  12107  suprcl  12114  suprub  12115  suprlub  12118  infrecl  12136  infregelb  12138  infrelb  12139  supfirege  12141  suprfinzcl  12618  uzinfi  12853  suprzcl2  12863  suprzub  12864  2resupmax  13115  infmrp1  13272  fseqsupcl  13912  ssnn0fi  13920  fsuppmapnn0fiublem  13925  isercolllem1  15600  isercolllem2  15601  summolem2  15651  zsum  15653  fsumcvg3  15664  mertenslem2  15820  prodmolem2  15870  zprod  15872  cnso  16184  gcdval  16435  dfgcd2  16485  lcmval  16531  lcmgcdlem  16545  odzval  16731  pczpre  16787  prmreclem1  16856  ramz  16965  odval  19475  odf  19478  gexval  19519  gsumval3  19848  retos  21585  mbfsup  25633  mbfinf  25634  itg2monolem1  25719  itg2mono  25722  dvgt0lem2  25976  dvgt0  25977  plyeq0lem  26183  dgrval  26201  dgrcl  26206  dgrub  26207  dgrlb  26209  elqaalem1  26295  elqaalem3  26297  aalioulem2  26309  logccv  26640  ex-po  30522  ssnnssfz  32878  lmdvg  34131  oddpwdc  34532  ballotlemi  34679  ballotlemiex  34680  ballotlemsup  34683  ballotlemimin  34684  ballotlemfrcn0  34708  ballotlemirc  34710  erdszelem3  35409  erdszelem4  35410  erdszelem5  35411  erdszelem6  35412  erdszelem8  35414  erdszelem9  35415  erdszelem11  35417  erdsze2lem1  35419  erdsze2lem2  35420  supfz  35945  inffz  35946  gtinf  36535  ptrecube  37871  poimirlem31  37902  poimirlem32  37903  heicant  37906  mblfinlem3  37910  mblfinlem4  37911  ismblfin  37912  incsequz2  38000  totbndbnd  38040  prdsbnd  38044  aks4d1p4  42449  aks4d1p7  42453  sticksstones1  42516  sticksstones3  42518  sn-suprcld  42863  sn-suprubd  42864  pellfundval  43237  dgraaval  43501  dgraaf  43504  fzisoeu  45662  uzublem  45788  infrglb  45950  limsupubuzlem  46070  fourierdlem25  46490  fourierdlem31  46496  fourierdlem36  46501  fourierdlem37  46502  fourierdlem42  46507  fourierdlem79  46543  ioorrnopnlem  46662  hoicvr  46906  hoidmvlelem2  46954  iunhoiioolem  47033  vonioolem1  47038  fsupdm2  47201  finfdm2  47205  chnsuslle  47239  prmdvdsfmtnof1lem1  47944  prmdvdsfmtnof  47946  prmdvdsfmtnof1  47947  ssnn0ssfz  48709  rrx2plordso  49084