Theorem climrel 15508

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

Syntax hints:   ∧ wa 395   ∈ wcel 2108  ∀wral 3051  ∃wrex 3060   class class class wbr 5119  Rel wrel 5659  ‘cfv 6531  (class class class)co 7405  ℂcc 11127   < clt 11269   − cmin 11466  ℤcz 12588  ℤ_≥cuz 12852  ℝ⁺crp 13008  abscabs 15253   ⇝ cli 15500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-opab 5182  df-xp 5660  df-rel 5661  df-clim 15504

This theorem is referenced by:  clim  15510  climcl  15515  climi  15526  climrlim2  15563  fclim  15569  climrecl  15599  climge0  15600  iserex  15673  caurcvg2  15694  caucvg  15695  iseralt  15701  fsumcvg3  15745  cvgcmpce  15834  climfsum  15836  climcnds  15867  trirecip  15879  ntrivcvgn0  15914  ovoliunlem1  25455  mbflimlem  25620  abelthlem5  26397  emcllem6  26963  lgamgulmlem4  26994  binomcxplemnn0  44373  binomcxplemnotnn0  44380  climf  45651  sumnnodd  45659  climf2  45695  climd  45701  clim2d  45702  climfv  45720  climuzlem  45772  climlimsup  45789  climlimsupcex  45798  climliminflimsupd  45830  climliminf  45835  liminflimsupclim  45836  xlimclimdm  45883  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  stirlinglem12  46114  fouriersw  46260