Theorem climrel 15528

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

Syntax hints:   ∧ wa 395   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070   class class class wbr 5143  Rel wrel 5690  ‘cfv 6561  (class class class)co 7431  ℂcc 11153   < clt 11295   − cmin 11492  ℤcz 12613  ℤ_≥cuz 12878  ℝ⁺crp 13034  abscabs 15273   ⇝ cli 15520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692  df-clim 15524

This theorem is referenced by:  clim  15530  climcl  15535  climi  15546  climrlim2  15583  fclim  15589  climrecl  15619  climge0  15620  iserex  15693  caurcvg2  15714  caucvg  15715  iseralt  15721  fsumcvg3  15765  cvgcmpce  15854  climfsum  15856  climcnds  15887  trirecip  15899  ntrivcvgn0  15934  ovoliunlem1  25537  mbflimlem  25702  abelthlem5  26479  emcllem6  27044  lgamgulmlem4  27075  binomcxplemnn0  44368  binomcxplemnotnn0  44375  climf  45637  sumnnodd  45645  climf2  45681  climd  45687  clim2d  45688  climfv  45706  climuzlem  45758  climlimsup  45775  climlimsupcex  45784  climliminflimsupd  45816  climliminf  45821  liminflimsupclim  45822  xlimclimdm  45869  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stirlinglem12  46100  fouriersw  46246