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

Theorem climrel 15309
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 15305 . 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 12696  +crp 12844  abscabs 15053  cli 15301
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 15305
This theorem is referenced by:  clim  15311  climcl  15316  climi  15327  climrlim2  15364  fclim  15370  climrecl  15400  climge0  15401  iserex  15476  caurcvg2  15497  caucvg  15498  iseralt  15504  fsumcvg3  15549  cvgcmpce  15638  climfsum  15640  climcnds  15671  trirecip  15683  ntrivcvgn0  15718  ovoliunlem1  24789  mbflimlem  24954  abelthlem5  25717  emcllem6  26273  lgamgulmlem4  26304  binomcxplemnn0  42394  binomcxplemnotnn0  42401  climf  43618  sumnnodd  43626  climf2  43662  climd  43668  clim2d  43669  climfv  43687  climuzlem  43739  climlimsup  43756  climlimsupcex  43765  climliminflimsupd  43797  climliminf  43802  liminflimsupclim  43803  xlimclimdm  43850  ioodvbdlimc1lem2  43928  ioodvbdlimc2lem  43930  stirlinglem12  44081  fouriersw  44227
  Copyright terms: Public domain W3C validator