Theorem climrel 15583

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088   class class class wbr 5107  Rel wrel 5664  ‘cfv 6537  (class class class)co 7417  ℂcc 11126   < clt 11271   − cmin 11469  ℤcz 12619  ℤ_≥cuz 12891  ℝ⁺crp 13046  abscabs 15325   ⇝ cli 15575

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-opab 5172  df-xp 5665  df-rel 5666  df-clim 15579

This theorem is used by:  clim  15585  climcl  15590  climi  15601  climrlim2  15638  fclim  15644  climrecl  15674  climge0  15675  iserex  15748  caurcvg2  15769  caucvg  15770  iseralt  15776  fsumcvg3  15819  cvgcmpce  15909  climfsum  15911  climcnds  15944  trirecip  15956  ntrivcvgn0  15991  ovoliunlem1  25736  mbflimlem  25901  abelthlem5  26678  emcllem6  27245  lgamgulmlem4  27276  binomcxplemnn0  45181  binomcxplemnotnn0  45188  climf  46460  sumnnodd  46468  climf2  46502  climd  46508  clim2d  46509  climfv  46527  climuzlem  46579  climlimsup  46596  climlimsupcex  46605  climliminflimsupd  46637  climliminf  46642  liminflimsupclim  46643  xlimclimdm  46690  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  stirlinglem12  46921  fouriersw  47067