Theorem climrel 15129

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 15125	. 2 ⊢ ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}
2	1	relopabiv 5719	1 ⊢ Rel ⇝

Syntax hints:   ∧ wa 395   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064   class class class wbr 5070  Rel wrel 5585  ‘cfv 6418  (class class class)co 7255  ℂcc 10800   < clt 10940   − cmin 11135  ℤcz 12249  ℤ_≥cuz 12511  ℝ⁺crp 12659  abscabs 14873   ⇝ cli 15121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586  df-rel 5587  df-clim 15125

This theorem is referenced by:  clim  15131  climcl  15136  climi  15147  climrlim2  15184  fclim  15190  climrecl  15220  climge0  15221  iserex  15296  caurcvg2  15317  caucvg  15318  iseralt  15324  fsumcvg3  15369  cvgcmpce  15458  climfsum  15460  climcnds  15491  trirecip  15503  ntrivcvgn0  15538  ovoliunlem1  24571  mbflimlem  24736  abelthlem5  25499  emcllem6  26055  lgamgulmlem4  26086  binomcxplemnn0  41856  binomcxplemnotnn0  41863  climf  43053  sumnnodd  43061  climf2  43097  climd  43103  clim2d  43104  climfv  43122  climuzlem  43174  climlimsup  43191  climlimsupcex  43200  climliminflimsupd  43232  climliminf  43237  liminflimsupclim  43238  xlimclimdm  43285  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stirlinglem12  43516  fouriersw  43662