Theorem ltso 11335

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

Syntax hints:   Or wor 5585  ℝcr 11148   < clt 11289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-resscn 11206  ax-pre-lttri 11223  ax-pre-lttrn 11224

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-opab 5208  df-mpt 5229  df-id 5572  df-po 5586  df-so 5587  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-er 8726  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11291  df-mnf 11292  df-ltxr 11294

This theorem is referenced by:  gtso  11336  lttri2  11337  lttri3  11338  lttri4  11339  ltnr  11350  ltnsym2  11354  fimaxre  12204  fiminre  12207  lbinf  12213  suprcl  12220  suprub  12221  suprlub  12224  infrecl  12242  infregelb  12244  infrelb  12245  supfirege  12247  suprfinzcl  12722  uzinfi  12958  suprzcl2  12968  suprzub  12969  2resupmax  13215  infmrp1  13371  fseqsupcl  13991  ssnn0fi  13999  fsuppmapnn0fiublem  14004  isercolllem1  15664  isercolllem2  15665  summolem2  15715  zsum  15717  fsumcvg3  15728  mertenslem2  15884  prodmolem2  15932  zprod  15934  cnso  16244  gcdval  16491  dfgcd2  16542  lcmval  16588  lcmgcdlem  16602  odzval  16788  pczpre  16844  prmreclem1  16913  ramz  17022  odval  19528  odf  19531  gexval  19572  gsumval3  19901  retos  21610  mbfsup  25681  mbfinf  25682  itg2monolem1  25768  itg2mono  25771  dvgt0lem2  26024  dvgt0  26025  plyeq0lem  26234  dgrval  26252  dgrcl  26257  dgrub  26258  dgrlb  26260  elqaalem1  26344  elqaalem3  26346  aalioulem2  26358  logccv  26687  ex-po  30365  ssnnssfz  32692  lmdvg  33781  oddpwdc  34201  ballotlemi  34347  ballotlemiex  34348  ballotlemsup  34351  ballotlemimin  34352  ballotlemfrcn0  34376  ballotlemirc  34378  erdszelem3  35034  erdszelem4  35035  erdszelem5  35036  erdszelem6  35037  erdszelem8  35039  erdszelem9  35040  erdszelem11  35042  erdsze2lem1  35044  erdsze2lem2  35045  supfz  35564  inffz  35565  gtinf  36044  ptrecube  37334  poimirlem31  37365  poimirlem32  37366  heicant  37369  mblfinlem3  37373  mblfinlem4  37374  ismblfin  37375  incsequz2  37463  totbndbnd  37503  prdsbnd  37507  aks4d1p4  41791  aks4d1p7  41795  sticksstones1  41858  sticksstones3  41860  sn-suprcld  42184  sn-suprubd  42185  pellfundval  42574  dgraaval  42842  dgraaf  42845  fzisoeu  44951  uzublem  45081  infrglb  45247  limsupubuzlem  45369  fourierdlem25  45789  fourierdlem31  45795  fourierdlem36  45800  fourierdlem37  45801  fourierdlem42  45806  fourierdlem79  45842  ioorrnopnlem  45961  hoicvr  46205  hoidmvlelem2  46253  iunhoiioolem  46332  vonioolem1  46337  fsupdm2  46500  finfdm2  46504  prmdvdsfmtnof1lem1  47192  prmdvdsfmtnof  47194  prmdvdsfmtnof1  47195  ssnn0ssfz  47764  rrx2plordso  48148