Theorem climrel 15427

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062   class class class wbr 5100  Rel wrel 5637  ‘cfv 6500  (class class class)co 7368  ℂcc 11036   < clt 11178   − cmin 11376  ℤcz 12500  ℤ_≥cuz 12763  ℝ⁺crp 12917  abscabs 15169   ⇝ cli 15419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-opab 5163  df-xp 5638  df-rel 5639  df-clim 15423

This theorem is referenced by:  clim  15429  climcl  15434  climi  15445  climrlim2  15482  fclim  15488  climrecl  15518  climge0  15519  iserex  15592  caurcvg2  15613  caucvg  15614  iseralt  15620  fsumcvg3  15664  cvgcmpce  15753  climfsum  15755  climcnds  15786  trirecip  15798  ntrivcvgn0  15833  ovoliunlem1  25471  mbflimlem  25636  abelthlem5  26413  emcllem6  26979  lgamgulmlem4  27010  binomcxplemnn0  44699  binomcxplemnotnn0  44706  climf  45976  sumnnodd  45984  climf2  46018  climd  46024  clim2d  46025  climfv  46043  climuzlem  46095  climlimsup  46112  climlimsupcex  46121  climliminflimsupd  46153  climliminf  46158  liminflimsupclim  46159  xlimclimdm  46206  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  stirlinglem12  46437  fouriersw  46583