Theorem ltso 11429

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

This proof depends on syntax axioms:   Or wor 5565  ℝcr 11238   < clt 11382

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-pre-lttri 11313  ax-pre-lttrn 11314

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-po 5566  df-so 5567  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-ltxr 11387

This theorem is used by:  gtso  11430  lttri2  11431  lttri3  11432  lttri4  11433  ltnr  11444  ltnsym2  11448  fimaxre  12301  fiminre  12304  lbinf  12310  suprcl  12317  suprub  12318  suprlub  12321  infrecl  12339  infregelb  12341  infrelb  12342  supfirege  12344  suprfinzcl  12853  uzinfi  13095  suprzcl2  13105  suprzub  13106  2resupmax  13358  infmrp1  13515  fseqsupcl  14160  ssnn0fi  14168  fsuppmapnn0fiublem  14173  isercolllem1  15876  isercolllem2  15877  summolem2  15926  zsum  15928  fsumcvg3  15939  mertenslem2  16098  prodmolem2  16146  zprod  16148  cnso  16459  gcdval  16710  dfgcd2  16763  lcmval  16811  lcmgcdlem  16825  odzval  17013  pczpre  17069  prmreclem1  17138  ramz  17247  odval  19799  odf  19802  gexval  19843  gsumval3  20172  retos  21979  mbfsup  26040  mbfinf  26041  itg2monolem1  26126  itg2mono  26129  dvgt0lem2  26378  dvgt0  26379  plyeq0lem  26584  dgrval  26602  dgrcl  26607  dgrub  26608  dgrlb  26610  elqaalem1  26699  elqaalem3  26701  aalioulem2  26717  logccv  27048  ex-po  31093  ssnnssfz  33475  lmdvg  34696  oddpwdc  35097  ballotlemi  35244  ballotlemiex  35245  ballotlemsup  35248  ballotlemimin  35249  ballotlemfrcn0  35273  ballotlemirc  35275  erdszelem3  36166  erdszelem4  36167  erdszelem5  36168  erdszelem6  36169  erdszelem8  36171  erdszelem9  36172  erdszelem11  36174  erdsze2lem1  36176  erdsze2lem2  36177  supfz  36709  inffz  36710  gtinf  37322  ptrecube  38806  poimirlem31  38837  poimirlem32  38838  heicant  38841  mblfinlem3  38845  mblfinlem4  38846  ismblfin  38847  incsequz2  38949  totbndbnd  38989  prdsbnd  38993  aks4d1p4  43395  aks4d1p7  43399  sticksstones1  43462  sticksstones3  43464  sn-suprcld  43823  sn-suprubd  43824  frlmnzcoordval  43919  frlmnzcoordcl  43921  frlmnzcoordn0  43923  pellfundval  44153  dgraaval  44411  dgraaf  44414  fzisoeu  46589  uzublem  46713  infrglb  46875  limsupubuzlem  46995  fourierdlem25  47415  fourierdlem31  47421  fourierdlem36  47426  fourierdlem37  47427  fourierdlem42  47432  fourierdlem79  47468  ioorrnopnlem  47587  hoicvr  47831  hoidmvlelem2  47879  iunhoiioolem  47958  vonioolem1  47963  fsupdm2  48126  finfdm2  48130  chnsuslle  48164  prmdvdsfmtnof1lem1  48942  prmdvdsfmtnof  48944  prmdvdsfmtnof1  48945  ssnn0ssfz  49792  rrx2plordso  50168