MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  climrel Structured version   Visualization version   GIF version

Theorem climrel 15310
Description: The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
Assertion
Ref Expression
climrel Rel ⇝

Proof of Theorem climrel
Dummy variables 𝑗 𝑘 𝑥 𝑦 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-clim 15306 . 2 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
21relopabiv 5773 1 Rel ⇝
Colors of variables: wff setvar class
Syntax hints:  wa 397  wcel 2107  wral 3063  wrex 3072   class class class wbr 5104  Rel wrel 5636  cfv 6492  (class class class)co 7350  cc 10983   < clt 11123  cmin 11319  cz 12433  cuz 12697  +crp 12845  abscabs 15054  cli 15302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-in 3916  df-ss 3926  df-opab 5167  df-xp 5637  df-rel 5638  df-clim 15306
This theorem is referenced by:  clim  15312  climcl  15317  climi  15328  climrlim2  15365  fclim  15371  climrecl  15401  climge0  15402  iserex  15477  caurcvg2  15498  caucvg  15499  iseralt  15505  fsumcvg3  15550  cvgcmpce  15639  climfsum  15641  climcnds  15672  trirecip  15684  ntrivcvgn0  15719  ovoliunlem1  24794  mbflimlem  24959  abelthlem5  25722  emcllem6  26278  lgamgulmlem4  26309  binomcxplemnn0  42430  binomcxplemnotnn0  42437  climf  43654  sumnnodd  43662  climf2  43698  climd  43704  clim2d  43705  climfv  43723  climuzlem  43775  climlimsup  43792  climlimsupcex  43801  climliminflimsupd  43833  climliminf  43838  liminflimsupclim  43839  xlimclimdm  43886  ioodvbdlimc1lem2  43964  ioodvbdlimc2lem  43966  stirlinglem12  44117  fouriersw  44263
  Copyright terms: Public domain W3C validator