Theorem climrel 15440

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

Syntax hints:   ∧ wa 394   ∈ wcel 2104  ∀wral 3059  ∃wrex 3068   class class class wbr 5147  Rel wrel 5680  ‘cfv 6542  (class class class)co 7411  ℂcc 11110   < clt 11252   − cmin 11448  ℤcz 12562  ℤ_≥cuz 12826  ℝ⁺crp 12978  abscabs 15185   ⇝ cli 15432

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-opab 5210  df-xp 5681  df-rel 5682  df-clim 15436

This theorem is referenced by:  clim  15442  climcl  15447  climi  15458  climrlim2  15495  fclim  15501  climrecl  15531  climge0  15532  iserex  15607  caurcvg2  15628  caucvg  15629  iseralt  15635  fsumcvg3  15679  cvgcmpce  15768  climfsum  15770  climcnds  15801  trirecip  15813  ntrivcvgn0  15848  ovoliunlem1  25251  mbflimlem  25416  abelthlem5  26183  emcllem6  26741  lgamgulmlem4  26772  binomcxplemnn0  43410  binomcxplemnotnn0  43417  climf  44636  sumnnodd  44644  climf2  44680  climd  44686  clim2d  44687  climfv  44705  climuzlem  44757  climlimsup  44774  climlimsupcex  44783  climliminflimsupd  44815  climliminf  44820  liminflimsupclim  44821  xlimclimdm  44868  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  stirlinglem12  45099  fouriersw  45245