Theorem climrel 15533

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

Syntax hints:   ∧ wa 400   ∈ wcel 2145  ∀wral 3079  ∃wrex 3089   class class class wbr 5105  Rel wrel 5657  ‘cfv 6525  (class class class)co 7400  ℂcc 11086   < clt 11231   − cmin 11429  ℤcz 12582  ℤ_≥cuz 12853  ℝ⁺crp 13007  abscabs 15275   ⇝ cli 15525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-opab 5168  df-xp 5658  df-rel 5659  df-clim 15529

This theorem is referenced by:  clim  15535  climcl  15540  climi  15551  climrlim2  15588  fclim  15594  climrecl  15624  climge0  15625  iserex  15698  caurcvg2  15719  caucvg  15720  iseralt  15726  fsumcvg3  15770  cvgcmpce  15860  climfsum  15862  climcnds  15895  trirecip  15907  ntrivcvgn0  15942  ovoliunlem1  25622  mbflimlem  25787  abelthlem5  26556  emcllem6  27123  lgamgulmlem4  27154  binomcxplemnn0  44923  binomcxplemnotnn0  44930  climf  46196  sumnnodd  46204  climf2  46238  climd  46244  clim2d  46245  climfv  46263  climuzlem  46315  climlimsup  46332  climlimsupcex  46341  climliminflimsupd  46373  climliminf  46378  liminflimsupclim  46379  xlimclimdm  46426  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  stirlinglem12  46657  fouriersw  46803