Theorem climrel 14897

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.

Step	Hyp	Ref	Expression
1		df-clim 14893	. 2 ⊢ ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}
2	1	relopabi 5663	1 ⊢ Rel ⇝

Syntax hints:   ∧ wa 399   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071   class class class wbr 5032  Rel wrel 5529  ‘cfv 6335  (class class class)co 7150  ℂcc 10573   < clt 10713   − cmin 10908  ℤcz 12020  ℤ_≥cuz 12282  ℝ⁺crp 12430  abscabs 14641   ⇝ cli 14889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-11 2158  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3863  df-in 3865  df-ss 3875  df-sn 4523  df-pr 4525  df-op 4529  df-opab 5095  df-xp 5530  df-rel 5531  df-clim 14893

This theorem is referenced by:  clim  14899  climcl  14904  climi  14915  climrlim2  14952  fclim  14958  climrecl  14988  climge0  14989  iserex  15061  caurcvg2  15082  caucvg  15083  iseralt  15089  fsumcvg3  15134  cvgcmpce  15221  climfsum  15223  climcnds  15254  trirecip  15266  ntrivcvgn0  15302  ovoliunlem1  24202  mbflimlem  24367  abelthlem5  25129  emcllem6  25685  lgamgulmlem4  25716  binomcxplemnn0  41426  binomcxplemnotnn0  41433  climf  42630  sumnnodd  42638  climf2  42674  climd  42680  clim2d  42681  climfv  42699  climuzlem  42751  climlimsup  42768  climlimsupcex  42777  climliminflimsupd  42809  climliminf  42814  liminflimsupclim  42815  xlimclimdm  42862  ioodvbdlimc1lem2  42940  ioodvbdlimc2lem  42942  stirlinglem12  43093  fouriersw  43239