Theorem climrel 15396

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

Syntax hints:   ∧ wa 395   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056   class class class wbr 5091  Rel wrel 5621  ‘cfv 6481  (class class class)co 7346  ℂcc 11001   < clt 11143   − cmin 11341  ℤcz 12465  ℤ_≥cuz 12729  ℝ⁺crp 12887  abscabs 15138   ⇝ cli 15388

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-opab 5154  df-xp 5622  df-rel 5623  df-clim 15392

This theorem is referenced by:  clim  15398  climcl  15403  climi  15414  climrlim2  15451  fclim  15457  climrecl  15487  climge0  15488  iserex  15561  caurcvg2  15582  caucvg  15583  iseralt  15589  fsumcvg3  15633  cvgcmpce  15722  climfsum  15724  climcnds  15755  trirecip  15767  ntrivcvgn0  15802  ovoliunlem1  25428  mbflimlem  25593  abelthlem5  26370  emcllem6  26936  lgamgulmlem4  26967  binomcxplemnn0  44381  binomcxplemnotnn0  44388  climf  45661  sumnnodd  45669  climf2  45703  climd  45709  clim2d  45710  climfv  45728  climuzlem  45780  climlimsup  45797  climlimsupcex  45806  climliminflimsupd  45838  climliminf  45843  liminflimsupclim  45844  xlimclimdm  45891  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  stirlinglem12  46122  fouriersw  46268