Theorem climrel 15524

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

Syntax hints:   ∧ wa 395   ∈ wcel 2105  ∀wral 3058  ∃wrex 3067   class class class wbr 5147  Rel wrel 5693  ‘cfv 6562  (class class class)co 7430  ℂcc 11150   < clt 11292   − cmin 11489  ℤcz 12610  ℤ_≥cuz 12875  ℝ⁺crp 13031  abscabs 15269   ⇝ cli 15516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-opab 5210  df-xp 5694  df-rel 5695  df-clim 15520

This theorem is referenced by:  clim  15526  climcl  15531  climi  15542  climrlim2  15579  fclim  15585  climrecl  15615  climge0  15616  iserex  15689  caurcvg2  15710  caucvg  15711  iseralt  15717  fsumcvg3  15761  cvgcmpce  15850  climfsum  15852  climcnds  15883  trirecip  15895  ntrivcvgn0  15930  ovoliunlem1  25550  mbflimlem  25715  abelthlem5  26493  emcllem6  27058  lgamgulmlem4  27089  binomcxplemnn0  44344  binomcxplemnotnn0  44351  climf  45577  sumnnodd  45585  climf2  45621  climd  45627  clim2d  45628  climfv  45646  climuzlem  45698  climlimsup  45715  climlimsupcex  45724  climliminflimsupd  45756  climliminf  45761  liminflimsupclim  45762  xlimclimdm  45809  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stirlinglem12  46040  fouriersw  46186