Theorem climrel 15401

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

Syntax hints:   ∧ wa 395   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057   class class class wbr 5093  Rel wrel 5624  ‘cfv 6486  (class class class)co 7352  ℂcc 11011   < clt 11153   − cmin 11351  ℤcz 12475  ℤ_≥cuz 12738  ℝ⁺crp 12892  abscabs 15143   ⇝ cli 15393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-opab 5156  df-xp 5625  df-rel 5626  df-clim 15397

This theorem is referenced by:  clim  15403  climcl  15408  climi  15419  climrlim2  15456  fclim  15462  climrecl  15492  climge0  15493  iserex  15566  caurcvg2  15587  caucvg  15588  iseralt  15594  fsumcvg3  15638  cvgcmpce  15727  climfsum  15729  climcnds  15760  trirecip  15772  ntrivcvgn0  15807  ovoliunlem1  25431  mbflimlem  25596  abelthlem5  26373  emcllem6  26939  lgamgulmlem4  26970  binomcxplemnn0  44466  binomcxplemnotnn0  44473  climf  45746  sumnnodd  45754  climf2  45788  climd  45794  clim2d  45795  climfv  45813  climuzlem  45865  climlimsup  45882  climlimsupcex  45891  climliminflimsupd  45923  climliminf  45928  liminflimsupclim  45929  xlimclimdm  45976  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  stirlinglem12  46207  fouriersw  46353