Theorem ltso 11314

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

This proof depends on syntax axioms:   Or wor 5562  ℝcr 11123   < clt 11267

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-pre-lttri 11198  ax-pre-lttrn 11199

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-ltxr 11272

This theorem is used by:  gtso  11315  lttri2  11316  lttri3  11317  lttri4  11318  ltnr  11329  ltnsym2  11333  fimaxre  12183  fiminre  12186  lbinf  12192  suprcl  12199  suprub  12200  suprlub  12203  infrecl  12221  infregelb  12223  infrelb  12224  supfirege  12226  suprfinzcl  12735  uzinfi  12977  suprzcl2  12987  suprzub  12988  2resupmax  13240  infmrp1  13397  fseqsupcl  14041  ssnn0fi  14049  fsuppmapnn0fiublem  14054  isercolllem1  15752  isercolllem2  15753  summolem2  15802  zsum  15804  fsumcvg3  15815  mertenslem2  15974  prodmolem2  16022  zprod  16024  cnso  16335  gcdval  16586  dfgcd2  16636  lcmval  16682  lcmgcdlem  16696  odzval  16883  pczpre  16939  prmreclem1  17008  ramz  17117  odval  19661  odf  19664  gexval  19705  gsumval3  20034  retos  21831  mbfsup  25892  mbfinf  25893  itg2monolem1  25978  itg2mono  25981  dvgt0lem2  26230  dvgt0  26231  plyeq0lem  26436  dgrval  26454  dgrcl  26459  dgrub  26460  dgrlb  26462  elqaalem1  26551  elqaalem3  26553  aalioulem2  26569  logccv  26900  ex-po  30915  ssnnssfz  33258  lmdvg  34463  oddpwdc  34865  ballotlemi  35012  ballotlemiex  35013  ballotlemsup  35016  ballotlemimin  35017  ballotlemfrcn0  35041  ballotlemirc  35043  erdszelem3  35772  erdszelem4  35773  erdszelem5  35774  erdszelem6  35775  erdszelem8  35777  erdszelem9  35778  erdszelem11  35780  erdsze2lem1  35782  erdsze2lem2  35783  supfz  36308  inffz  36309  gtinf  36938  ptrecube  38369  poimirlem31  38400  poimirlem32  38401  heicant  38404  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  incsequz2  38499  totbndbnd  38539  prdsbnd  38543  aks4d1p4  42945  aks4d1p7  42949  sticksstones1  43012  sticksstones3  43014  sn-suprcld  43381  sn-suprubd  43382  pellfundval  43721  dgraaval  43985  dgraaf  43988  fzisoeu  46133  uzublem  46258  infrglb  46420  limsupubuzlem  46540  fourierdlem25  46960  fourierdlem31  46966  fourierdlem36  46971  fourierdlem37  46972  fourierdlem42  46977  fourierdlem79  47013  ioorrnopnlem  47132  hoicvr  47376  hoidmvlelem2  47424  iunhoiioolem  47503  vonioolem1  47508  fsupdm2  47671  finfdm2  47675  chnsuslle  47709  prmdvdsfmtnof1lem1  48487  prmdvdsfmtnof  48489  prmdvdsfmtnof1  48490  ssnn0ssfz  49279  rrx2plordso  49654