Theorem ltso 11305

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

This proof depends on syntax axioms:   Or wor 5570  ℝcr 11114   < clt 11258

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11172  ax-pre-lttri 11189  ax-pre-lttrn 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11260  df-mnf 11261  df-ltxr 11263

This theorem is used by:  gtso  11306  lttri2  11307  lttri3  11308  lttri4  11309  ltnr  11320  ltnsym2  11324  fimaxre  12174  fiminre  12177  lbinf  12183  suprcl  12190  suprub  12191  suprlub  12194  infrecl  12212  infregelb  12214  infrelb  12215  supfirege  12217  suprfinzcl  12726  uzinfi  12968  suprzcl2  12978  suprzub  12979  2resupmax  13230  infmrp1  13387  fseqsupcl  14031  ssnn0fi  14039  fsuppmapnn0fiublem  14044  isercolllem1  15740  isercolllem2  15741  summolem2  15790  zsum  15792  fsumcvg3  15803  mertenslem2  15962  prodmolem2  16012  zprod  16014  cnso  16325  gcdval  16576  dfgcd2  16626  lcmval  16672  lcmgcdlem  16686  odzval  16873  pczpre  16929  prmreclem1  16998  ramz  17107  odval  19648  odf  19651  gexval  19692  gsumval3  20021  retos  21818  mbfsup  25874  mbfinf  25875  itg2monolem1  25960  itg2mono  25963  dvgt0lem2  26213  dvgt0  26214  plyeq0lem  26418  dgrval  26436  dgrcl  26441  dgrub  26442  dgrlb  26444  elqaalem1  26531  elqaalem3  26533  aalioulem2  26547  logccv  26879  ex-po  30857  ssnnssfz  33202  lmdvg  34407  oddpwdc  34809  ballotlemi  34956  ballotlemiex  34957  ballotlemsup  34960  ballotlemimin  34961  ballotlemfrcn0  34985  ballotlemirc  34987  erdszelem3  35722  erdszelem4  35723  erdszelem5  35724  erdszelem6  35725  erdszelem8  35727  erdszelem9  35728  erdszelem11  35730  erdsze2lem1  35732  erdsze2lem2  35733  supfz  36258  inffz  36259  gtinf  36887  ptrecube  38328  poimirlem31  38359  poimirlem32  38360  heicant  38363  mblfinlem3  38367  mblfinlem4  38368  ismblfin  38369  incsequz2  38458  totbndbnd  38498  prdsbnd  38502  aks4d1p4  42904  aks4d1p7  42908  sticksstones1  42971  sticksstones3  42973  sn-suprcld  43325  sn-suprubd  43326  pellfundval  43665  dgraaval  43929  dgraaf  43932  fzisoeu  46077  uzublem  46202  infrglb  46364  limsupubuzlem  46484  fourierdlem25  46904  fourierdlem31  46910  fourierdlem36  46915  fourierdlem37  46916  fourierdlem42  46921  fourierdlem79  46957  ioorrnopnlem  47076  hoicvr  47320  hoidmvlelem2  47368  iunhoiioolem  47447  vonioolem1  47452  fsupdm2  47615  finfdm2  47619  chnsuslle  47655  prmdvdsfmtnof1lem1  48394  prmdvdsfmtnof  48396  prmdvdsfmtnof1  48397  ssnn0ssfz  49186  rrx2plordso  49561