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

Theorem climrel 14424
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 14420 . 2 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
21relopabi 5382 1 Rel ⇝
Colors of variables: wff setvar class
Syntax hints:  wa 382  wcel 2145  wral 3061  wrex 3062   class class class wbr 4786  Rel wrel 5254  cfv 6029  (class class class)co 6791  cc 10134   < clt 10274  cmin 10466  cz 11577  cuz 11886  +crp 12028  abscabs 14175  cli 14416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-opab 4847  df-xp 5255  df-rel 5256  df-clim 14420
This theorem is referenced by:  clim  14426  climcl  14431  climi  14442  climrlim2  14479  fclim  14485  climrecl  14515  climge0  14516  iserex  14588  caurcvg2  14609  caucvg  14610  iseralt  14616  fsumcvg3  14661  cvgcmpce  14750  climfsum  14752  climcnds  14783  trirecip  14795  ntrivcvgn0  14830  ovoliunlem1  23483  mbflimlem  23647  abelthlem5  24402  emcllem6  24941  lgamgulmlem4  24972  binomcxplemnn0  39067  binomcxplemnotnn0  39074  climf  40365  sumnnodd  40373  climf2  40409  climd  40415  clim2d  40416  climfv  40434  climuzlem  40486  climlimsup  40503  climlimsupcex  40512  climliminflimsupd  40544  climliminf  40549  liminflimsupclim  40550  ioodvbdlimc1lem2  40658  ioodvbdlimc2lem  40660  stirlinglem12  40812  fouriersw  40958
  Copyright terms: Public domain W3C validator