Theorem climrel 15452

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

Syntax hints:   ∧ wa 396   ∈ wcel 2119  ∀wral 3054  ∃wrex 3064   class class class wbr 5079  Rel wrel 5630  ‘cfv 6492  (class class class)co 7363  ℂcc 11034   < clt 11177   − cmin 11375  ℤcz 12522  ℤ_≥cuz 12786  ℝ⁺crp 12940  abscabs 15194   ⇝ cli 15444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-opab 5142  df-xp 5631  df-rel 5632  df-clim 15448

This theorem is referenced by:  clim  15454  climcl  15459  climi  15470  climrlim2  15507  fclim  15513  climrecl  15543  climge0  15544  iserex  15617  caurcvg2  15638  caucvg  15639  iseralt  15645  fsumcvg3  15689  cvgcmpce  15779  climfsum  15781  climcnds  15814  trirecip  15826  ntrivcvgn0  15861  ovoliunlem1  25494  mbflimlem  25659  abelthlem5  26425  emcllem6  26989  lgamgulmlem4  27020  binomcxplemnn0  44800  binomcxplemnotnn0  44807  climf  46074  sumnnodd  46082  climf2  46116  climd  46122  clim2d  46123  climfv  46141  climuzlem  46193  climlimsup  46210  climlimsupcex  46219  climliminflimsupd  46251  climliminf  46256  liminflimsupclim  46257  xlimclimdm  46304  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  stirlinglem12  46535  fouriersw  46681