Theorem climrel 15210

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

Syntax hints:   ∧ wa 396   ∈ wcel 2107  ∀wral 3065  ∃wrex 3066   class class class wbr 5075  Rel wrel 5595  ‘cfv 6437  (class class class)co 7284  ℂcc 10878   < clt 11018   − cmin 11214  ℤcz 12328  ℤ_≥cuz 12591  ℝ⁺crp 12739  abscabs 14954   ⇝ cli 15202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-opab 5138  df-xp 5596  df-rel 5597  df-clim 15206

This theorem is referenced by:  clim  15212  climcl  15217  climi  15228  climrlim2  15265  fclim  15271  climrecl  15301  climge0  15302  iserex  15377  caurcvg2  15398  caucvg  15399  iseralt  15405  fsumcvg3  15450  cvgcmpce  15539  climfsum  15541  climcnds  15572  trirecip  15584  ntrivcvgn0  15619  ovoliunlem1  24675  mbflimlem  24840  abelthlem5  25603  emcllem6  26159  lgamgulmlem4  26190  binomcxplemnn0  41974  binomcxplemnotnn0  41981  climf  43170  sumnnodd  43178  climf2  43214  climd  43220  clim2d  43221  climfv  43239  climuzlem  43291  climlimsup  43308  climlimsupcex  43317  climliminflimsupd  43349  climliminf  43354  liminflimsupclim  43355  xlimclimdm  43402  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  stirlinglem12  43633  fouriersw  43779