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

Theorem climrel 14157
 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 14153 . 2 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
21relopabi 5205 1 Rel ⇝
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 384   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908   class class class wbr 4613  Rel wrel 5079  ‘cfv 5847  (class class class)co 6604  ℂcc 9878   < clt 10018   − cmin 10210  ℤcz 11321  ℤ≥cuz 11631  ℝ+crp 11776  abscabs 13908   ⇝ cli 14149 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-opab 4674  df-xp 5080  df-rel 5081  df-clim 14153 This theorem is referenced by:  clim  14159  climcl  14164  climi  14175  climrlim2  14212  fclim  14218  climrecl  14248  climge0  14249  iserex  14321  caurcvg2  14342  caucvg  14343  iseralt  14349  fsumcvg3  14393  cvgcmpce  14477  climfsum  14479  climcnds  14508  trirecip  14520  ntrivcvgn0  14555  ovoliunlem1  23177  mbflimlem  23340  abelthlem5  24093  emcllem6  24627  lgamgulmlem4  24658  binomcxplemnn0  38030  binomcxplemnotnn0  38037  climf  39258  sumnnodd  39266  climf2  39302  climd  39308  clim2d  39309  climfv  39327  ioodvbdlimc1lem2  39453  ioodvbdlimc2lem  39455  stirlinglem12  39609  fouriersw  39755
 Copyright terms: Public domain W3C validator