Theorem climrel 15569

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2146  ∀wral 3082  ∃wrex 3092   class class class wbr 5114  Rel wrel 5671  ‘cfv 6543  (class class class)co 7423  ℂcc 11116   < clt 11261   − cmin 11459  ℤcz 12609  ℤ_≥cuz 12880  ℝ⁺crp 13034  abscabs 15311   ⇝ cli 15561

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-opab 5179  df-xp 5672  df-rel 5673  df-clim 15565

This theorem is used by:  clim  15571  climcl  15576  climi  15587  climrlim2  15624  fclim  15630  climrecl  15660  climge0  15661  iserex  15734  caurcvg2  15755  caucvg  15756  iseralt  15762  fsumcvg3  15806  cvgcmpce  15896  climfsum  15898  climcnds  15931  trirecip  15943  ntrivcvgn0  15978  ovoliunlem1  25698  mbflimlem  25863  abelthlem5  26635  emcllem6  27202  lgamgulmlem4  27233  binomcxplemnn0  45100  binomcxplemnotnn0  45107  climf  46379  sumnnodd  46387  climf2  46421  climd  46427  clim2d  46428  climfv  46446  climuzlem  46498  climlimsup  46515  climlimsupcex  46524  climliminflimsupd  46556  climliminf  46561  liminflimsupclim  46562  xlimclimdm  46609  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  stirlinglem12  46840  fouriersw  46986