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

Theorem climrel 14837
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 14833 . 2 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
21relopabi 5687 1 Rel ⇝
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2105  wral 3135  wrex 3136   class class class wbr 5057  Rel wrel 5553  cfv 6348  (class class class)co 7145  cc 10523   < clt 10663  cmin 10858  cz 11969  cuz 12231  +crp 12377  abscabs 14581  cli 14829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-opab 5120  df-xp 5554  df-rel 5555  df-clim 14833
This theorem is referenced by:  clim  14839  climcl  14844  climi  14855  climrlim2  14892  fclim  14898  climrecl  14928  climge0  14929  iserex  15001  caurcvg2  15022  caucvg  15023  iseralt  15029  fsumcvg3  15074  cvgcmpce  15161  climfsum  15163  climcnds  15194  trirecip  15206  ntrivcvgn0  15242  ovoliunlem1  24030  mbflimlem  24195  abelthlem5  24950  emcllem6  25505  lgamgulmlem4  25536  binomcxplemnn0  40558  binomcxplemnotnn0  40565  climf  41779  sumnnodd  41787  climf2  41823  climd  41829  clim2d  41830  climfv  41848  climuzlem  41900  climlimsup  41917  climlimsupcex  41926  climliminflimsupd  41958  climliminf  41963  liminflimsupclim  41964  xlimclimdm  42011  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  stirlinglem12  42247  fouriersw  42393
  Copyright terms: Public domain W3C validator