Theorem climrel 15454

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061   class class class wbr 5085  Rel wrel 5636  ‘cfv 6498  (class class class)co 7367  ℂcc 11036   < clt 11179   − cmin 11377  ℤcz 12524  ℤ_≥cuz 12788  ℝ⁺crp 12942  abscabs 15196   ⇝ cli 15446

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-opab 5148  df-xp 5637  df-rel 5638  df-clim 15450

This theorem is referenced by:  clim  15456  climcl  15461  climi  15472  climrlim2  15509  fclim  15515  climrecl  15545  climge0  15546  iserex  15619  caurcvg2  15640  caucvg  15641  iseralt  15647  fsumcvg3  15691  cvgcmpce  15781  climfsum  15783  climcnds  15816  trirecip  15828  ntrivcvgn0  15863  ovoliunlem1  25469  mbflimlem  25634  abelthlem5  26400  emcllem6  26964  lgamgulmlem4  26995  binomcxplemnn0  44776  binomcxplemnotnn0  44783  climf  46052  sumnnodd  46060  climf2  46094  climd  46100  clim2d  46101  climfv  46119  climuzlem  46171  climlimsup  46188  climlimsupcex  46197  climliminflimsupd  46229  climliminf  46234  liminflimsupclim  46235  xlimclimdm  46282  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stirlinglem12  46513  fouriersw  46659