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

Theorem climrel 14564
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 14560 . 2 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
21relopabi 5449 1 Rel ⇝
Colors of variables: wff setvar class
Syntax hints:  wa 385  wcel 2157  wral 3089  wrex 3090   class class class wbr 4843  Rel wrel 5317  cfv 6101  (class class class)co 6878  cc 10222   < clt 10363  cmin 10556  cz 11666  cuz 11930  +crp 12074  abscabs 14315  cli 14556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-opab 4906  df-xp 5318  df-rel 5319  df-clim 14560
This theorem is referenced by:  clim  14566  climcl  14571  climi  14582  climrlim2  14619  fclim  14625  climrecl  14655  climge0  14656  iserex  14728  caurcvg2  14749  caucvg  14750  iseralt  14756  fsumcvg3  14801  cvgcmpce  14888  climfsum  14890  climcnds  14921  trirecip  14933  ntrivcvgn0  14967  ovoliunlem1  23610  mbflimlem  23775  abelthlem5  24530  emcllem6  25079  lgamgulmlem4  25110  binomcxplemnn0  39330  binomcxplemnotnn0  39337  climf  40598  sumnnodd  40606  climf2  40642  climd  40648  clim2d  40649  climfv  40667  climuzlem  40719  climlimsup  40736  climlimsupcex  40745  climliminflimsupd  40777  climliminf  40782  liminflimsupclim  40783  ioodvbdlimc1lem2  40891  ioodvbdlimc2lem  40893  stirlinglem12  41045  fouriersw  41191
  Copyright terms: Public domain W3C validator