Theorem climrel 15495

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

Syntax hints:   ∧ wa 395   ∈ wcel 2107  ∀wral 3050  ∃wrex 3059   class class class wbr 5116  Rel wrel 5656  ‘cfv 6527  (class class class)co 7399  ℂcc 11119   < clt 11261   − cmin 11458  ℤcz 12580  ℤ_≥cuz 12844  ℝ⁺crp 13000  abscabs 15240   ⇝ cli 15487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3459  df-ss 3941  df-opab 5179  df-xp 5657  df-rel 5658  df-clim 15491

This theorem is referenced by:  clim  15497  climcl  15502  climi  15513  climrlim2  15550  fclim  15556  climrecl  15586  climge0  15587  iserex  15660  caurcvg2  15681  caucvg  15682  iseralt  15688  fsumcvg3  15732  cvgcmpce  15821  climfsum  15823  climcnds  15854  trirecip  15866  ntrivcvgn0  15901  ovoliunlem1  25440  mbflimlem  25605  abelthlem5  26382  emcllem6  26947  lgamgulmlem4  26978  binomcxplemnn0  44299  binomcxplemnotnn0  44306  climf  45581  sumnnodd  45589  climf2  45625  climd  45631  clim2d  45632  climfv  45650  climuzlem  45702  climlimsup  45719  climlimsupcex  45728  climliminflimsupd  45760  climliminf  45765  liminflimsupclim  45766  xlimclimdm  45813  ioodvbdlimc1lem2  45891  ioodvbdlimc2lem  45893  stirlinglem12  46044  fouriersw  46190