Theorem climrel 15664

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086   class class class wbr 5102  Rel wrel 5655  ‘cfv 6538  (class class class)co 7420  ℂcc 11201   < clt 11346   − cmin 11544  ℤcz 12696  ℤ_≥cuz 12968  ℝ⁺crp 13123  abscabs 15406   ⇝ cli 15656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-opab 5167  df-xp 5656  df-rel 5657  df-clim 15660

This theorem is used by:  clim  15666  climcl  15671  climi  15682  climrlim2  15719  fclim  15725  climrecl  15755  climge0  15756  iserex  15829  caurcvg2  15850  caucvg  15851  iseralt  15857  fsumcvg3  15900  cvgcmpce  15990  climfsum  15992  climcnds  16025  trirecip  16037  ntrivcvgn0  16072  ovoliunlem1  25828  mbflimlem  25993  abelthlem5  26767  emcllem6  27333  lgamgulmlem4  27364  binomcxplemnn0  45426  binomcxplemnotnn0  45433  climf  46727  sumnnodd  46735  climf2  46769  climd  46775  clim2d  46776  climfv  46794  climuzlem  46846  climlimsup  46863  climlimsupcex  46872  climliminflimsupd  46904  climliminf  46909  liminflimsupclim  46910  xlimclimdm  46957  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  stirlinglem12  47188  fouriersw  47334