Theorem climrel 15417

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053   class class class wbr 5095  Rel wrel 5628  ‘cfv 6486  (class class class)co 7353  ℂcc 11026   < clt 11168   − cmin 11365  ℤcz 12489  ℤ_≥cuz 12753  ℝ⁺crp 12911  abscabs 15159   ⇝ cli 15409

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 3440  df-ss 3922  df-opab 5158  df-xp 5629  df-rel 5630  df-clim 15413

This theorem is referenced by:  clim  15419  climcl  15424  climi  15435  climrlim2  15472  fclim  15478  climrecl  15508  climge0  15509  iserex  15582  caurcvg2  15603  caucvg  15604  iseralt  15610  fsumcvg3  15654  cvgcmpce  15743  climfsum  15745  climcnds  15776  trirecip  15788  ntrivcvgn0  15823  ovoliunlem1  25419  mbflimlem  25584  abelthlem5  26361  emcllem6  26927  lgamgulmlem4  26958  binomcxplemnn0  44322  binomcxplemnotnn0  44329  climf  45604  sumnnodd  45612  climf2  45648  climd  45654  clim2d  45655  climfv  45673  climuzlem  45725  climlimsup  45742  climlimsupcex  45751  climliminflimsupd  45783  climliminf  45788  liminflimsupclim  45789  xlimclimdm  45836  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  stirlinglem12  46067  fouriersw  46213