Theorem climrel 15415

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

Syntax hints:   ∧ wa 395   ∈ wcel 2113  ∀wral 3051  ∃wrex 3060   class class class wbr 5098  Rel wrel 5629  ‘cfv 6492  (class class class)co 7358  ℂcc 11024   < clt 11166   − cmin 11364  ℤcz 12488  ℤ_≥cuz 12751  ℝ⁺crp 12905  abscabs 15157   ⇝ cli 15407

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-opab 5161  df-xp 5630  df-rel 5631  df-clim 15411

This theorem is referenced by:  clim  15417  climcl  15422  climi  15433  climrlim2  15470  fclim  15476  climrecl  15506  climge0  15507  iserex  15580  caurcvg2  15601  caucvg  15602  iseralt  15608  fsumcvg3  15652  cvgcmpce  15741  climfsum  15743  climcnds  15774  trirecip  15786  ntrivcvgn0  15821  ovoliunlem1  25459  mbflimlem  25624  abelthlem5  26401  emcllem6  26967  lgamgulmlem4  26998  binomcxplemnn0  44586  binomcxplemnotnn0  44593  climf  45864  sumnnodd  45872  climf2  45906  climd  45912  clim2d  45913  climfv  45931  climuzlem  45983  climlimsup  46000  climlimsupcex  46009  climliminflimsupd  46041  climliminf  46046  liminflimsupclim  46047  xlimclimdm  46094  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  stirlinglem12  46325  fouriersw  46471