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

Theorem climrel 14844
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 14840 . 2 ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
21relopabi 5693 1 Rel ⇝
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2107  wral 3143  wrex 3144   class class class wbr 5063  Rel wrel 5559  cfv 6354  (class class class)co 7150  cc 10529   < clt 10669  cmin 10864  cz 11975  cuz 12237  +crp 12384  abscabs 14588  cli 14836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-opab 5126  df-xp 5560  df-rel 5561  df-clim 14840
This theorem is referenced by:  clim  14846  climcl  14851  climi  14862  climrlim2  14899  fclim  14905  climrecl  14935  climge0  14936  iserex  15008  caurcvg2  15029  caucvg  15030  iseralt  15036  fsumcvg3  15081  cvgcmpce  15168  climfsum  15170  climcnds  15201  trirecip  15213  ntrivcvgn0  15249  ovoliunlem1  24037  mbflimlem  24202  abelthlem5  24957  emcllem6  25511  lgamgulmlem4  25542  binomcxplemnn0  40565  binomcxplemnotnn0  40572  climf  41787  sumnnodd  41795  climf2  41831  climd  41837  clim2d  41838  climfv  41856  climuzlem  41908  climlimsup  41925  climlimsupcex  41934  climliminflimsupd  41966  climliminf  41971  liminflimsupclim  41972  xlimclimdm  42019  ioodvbdlimc1lem2  42101  ioodvbdlimc2lem  42103  stirlinglem12  42255  fouriersw  42401
  Copyright terms: Public domain W3C validator