Theorem climrel 15445

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062   class class class wbr 5086  Rel wrel 5629  ‘cfv 6492  (class class class)co 7360  ℂcc 11027   < clt 11170   − cmin 11368  ℤcz 12515  ℤ_≥cuz 12779  ℝ⁺crp 12933  abscabs 15187   ⇝ cli 15437

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-opab 5149  df-xp 5630  df-rel 5631  df-clim 15441

This theorem is referenced by:  clim  15447  climcl  15452  climi  15463  climrlim2  15500  fclim  15506  climrecl  15536  climge0  15537  iserex  15610  caurcvg2  15631  caucvg  15632  iseralt  15638  fsumcvg3  15682  cvgcmpce  15772  climfsum  15774  climcnds  15807  trirecip  15819  ntrivcvgn0  15854  ovoliunlem1  25479  mbflimlem  25644  abelthlem5  26413  emcllem6  26978  lgamgulmlem4  27009  binomcxplemnn0  44794  binomcxplemnotnn0  44801  climf  46070  sumnnodd  46078  climf2  46112  climd  46118  clim2d  46119  climfv  46137  climuzlem  46189  climlimsup  46206  climlimsupcex  46215  climliminflimsupd  46247  climliminf  46252  liminflimsupclim  46253  xlimclimdm  46300  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  stirlinglem12  46531  fouriersw  46677