Theorem climrel 15545

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

Syntax hints:   ∧ wa 400   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089   class class class wbr 5110  Rel wrel 5668  ‘cfv 6538  (class class class)co 7412  ℂcc 11099   < clt 11244   − cmin 11442  ℤcz 12592  ℤ_≥cuz 12863  ℝ⁺crp 13017  abscabs 15287   ⇝ cli 15537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-opab 5175  df-xp 5669  df-rel 5670  df-clim 15541

This theorem is referenced by:  clim  15547  climcl  15552  climi  15563  climrlim2  15600  fclim  15606  climrecl  15636  climge0  15637  iserex  15710  caurcvg2  15731  caucvg  15732  iseralt  15738  fsumcvg3  15782  cvgcmpce  15872  climfsum  15874  climcnds  15907  trirecip  15919  ntrivcvgn0  15954  ovoliunlem1  25642  mbflimlem  25807  abelthlem5  26579  emcllem6  27146  lgamgulmlem4  27177  binomcxplemnn0  45042  binomcxplemnotnn0  45049  climf  46321  sumnnodd  46329  climf2  46363  climd  46369  clim2d  46370  climfv  46388  climuzlem  46440  climlimsup  46457  climlimsupcex  46466  climliminflimsupd  46498  climliminf  46503  liminflimsupclim  46504  xlimclimdm  46551  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  stirlinglem12  46782  fouriersw  46928