Theorem ltso 11226

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

Syntax hints:   Or wor 5538  ℝcr 11037   < clt 11179

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184

This theorem is referenced by:  gtso  11227  lttri2  11228  lttri3  11229  lttri4  11230  ltnr  11241  ltnsym2  11245  fimaxre  12100  fiminre  12103  lbinf  12109  suprcl  12116  suprub  12117  suprlub  12120  infrecl  12138  infregelb  12140  infrelb  12141  supfirege  12143  suprfinzcl  12643  uzinfi  12878  suprzcl2  12888  suprzub  12889  2resupmax  13140  infmrp1  13297  fseqsupcl  13939  ssnn0fi  13947  fsuppmapnn0fiublem  13952  isercolllem1  15627  isercolllem2  15628  summolem2  15678  zsum  15680  fsumcvg3  15691  mertenslem2  15850  prodmolem2  15900  zprod  15902  cnso  16214  gcdval  16465  dfgcd2  16515  lcmval  16561  lcmgcdlem  16575  odzval  16762  pczpre  16818  prmreclem1  16887  ramz  16996  odval  19509  odf  19512  gexval  19553  gsumval3  19882  retos  21598  mbfsup  25631  mbfinf  25632  itg2monolem1  25717  itg2mono  25720  dvgt0lem2  25970  dvgt0  25971  plyeq0lem  26175  dgrval  26193  dgrcl  26198  dgrub  26199  dgrlb  26201  elqaalem1  26285  elqaalem3  26287  aalioulem2  26299  logccv  26627  ex-po  30505  ssnnssfz  32860  lmdvg  34097  oddpwdc  34498  ballotlemi  34645  ballotlemiex  34646  ballotlemsup  34649  ballotlemimin  34650  ballotlemfrcn0  34674  ballotlemirc  34676  erdszelem3  35375  erdszelem4  35376  erdszelem5  35377  erdszelem6  35378  erdszelem8  35380  erdszelem9  35381  erdszelem11  35383  erdsze2lem1  35385  erdsze2lem2  35386  supfz  35911  inffz  35912  gtinf  36501  ptrecube  37941  poimirlem31  37972  poimirlem32  37973  heicant  37976  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  incsequz2  38070  totbndbnd  38110  prdsbnd  38114  aks4d1p4  42518  aks4d1p7  42522  sticksstones1  42585  sticksstones3  42587  sn-suprcld  42938  sn-suprubd  42939  pellfundval  43308  dgraaval  43572  dgraaf  43575  fzisoeu  45733  uzublem  45858  infrglb  46020  limsupubuzlem  46140  fourierdlem25  46560  fourierdlem31  46566  fourierdlem36  46571  fourierdlem37  46572  fourierdlem42  46577  fourierdlem79  46613  ioorrnopnlem  46732  hoicvr  46976  hoidmvlelem2  47024  iunhoiioolem  47103  vonioolem1  47108  fsupdm2  47271  finfdm2  47275  chnsuslle  47311  prmdvdsfmtnof1lem1  48047  prmdvdsfmtnof  48049  prmdvdsfmtnof1  48050  ssnn0ssfz  48825  rrx2plordso  49200