Theorem climrel 15386

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

Syntax hints:   ∧ wa 396   ∈ wcel 2106  ∀wral 3060  ∃wrex 3069   class class class wbr 5110  Rel wrel 5643  ‘cfv 6501  (class class class)co 7362  ℂcc 11058   < clt 11198   − cmin 11394  ℤcz 12508  ℤ_≥cuz 12772  ℝ⁺crp 12924  abscabs 15131   ⇝ cli 15378

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-opab 5173  df-xp 5644  df-rel 5645  df-clim 15382

This theorem is referenced by:  clim  15388  climcl  15393  climi  15404  climrlim2  15441  fclim  15447  climrecl  15477  climge0  15478  iserex  15553  caurcvg2  15574  caucvg  15575  iseralt  15581  fsumcvg3  15625  cvgcmpce  15714  climfsum  15716  climcnds  15747  trirecip  15759  ntrivcvgn0  15794  ovoliunlem1  24903  mbflimlem  25068  abelthlem5  25831  emcllem6  26387  lgamgulmlem4  26418  binomcxplemnn0  42751  binomcxplemnotnn0  42758  climf  43983  sumnnodd  43991  climf2  44027  climd  44033  clim2d  44034  climfv  44052  climuzlem  44104  climlimsup  44121  climlimsupcex  44130  climliminflimsupd  44162  climliminf  44167  liminflimsupclim  44168  xlimclimdm  44215  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  stirlinglem12  44446  fouriersw  44592