Theorem climrel 15639

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087   class class class wbr 5103  Rel wrel 5656  ‘cfv 6531  (class class class)co 7412  ℂcc 11179   < clt 11324   − cmin 11522  ℤcz 12674  ℤ_≥cuz 12946  ℝ⁺crp 13101  abscabs 15381   ⇝ cli 15631

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-opab 5168  df-xp 5657  df-rel 5658  df-clim 15635

This theorem is used by:  clim  15641  climcl  15646  climi  15657  climrlim2  15694  fclim  15700  climrecl  15730  climge0  15731  iserex  15804  caurcvg2  15825  caucvg  15826  iseralt  15832  fsumcvg3  15875  cvgcmpce  15965  climfsum  15967  climcnds  16000  trirecip  16012  ntrivcvgn0  16047  ovoliunlem1  25803  mbflimlem  25968  abelthlem5  26744  emcllem6  27310  lgamgulmlem4  27341  binomcxplemnn0  45292  binomcxplemnotnn0  45299  climf  46578  sumnnodd  46586  climf2  46620  climd  46626  clim2d  46627  climfv  46645  climuzlem  46697  climlimsup  46714  climlimsupcex  46723  climliminflimsupd  46755  climliminf  46760  liminflimsupclim  46761  xlimclimdm  46808  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  stirlinglem12  47039  fouriersw  47185