Theorem climrel 15458

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053   class class class wbr 5107  Rel wrel 5643  ‘cfv 6511  (class class class)co 7387  ℂcc 11066   < clt 11208   − cmin 11405  ℤcz 12529  ℤ_≥cuz 12793  ℝ⁺crp 12951  abscabs 15200   ⇝ cli 15450

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645  df-clim 15454

This theorem is referenced by:  clim  15460  climcl  15465  climi  15476  climrlim2  15513  fclim  15519  climrecl  15549  climge0  15550  iserex  15623  caurcvg2  15644  caucvg  15645  iseralt  15651  fsumcvg3  15695  cvgcmpce  15784  climfsum  15786  climcnds  15817  trirecip  15829  ntrivcvgn0  15864  ovoliunlem1  25403  mbflimlem  25568  abelthlem5  26345  emcllem6  26911  lgamgulmlem4  26942  binomcxplemnn0  44338  binomcxplemnotnn0  44345  climf  45620  sumnnodd  45628  climf2  45664  climd  45670  clim2d  45671  climfv  45689  climuzlem  45741  climlimsup  45758  climlimsupcex  45767  climliminflimsupd  45799  climliminf  45804  liminflimsupclim  45805  xlimclimdm  45852  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stirlinglem12  46083  fouriersw  46229