Theorem climrel 14564

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

Syntax hints:   ∧ wa 385   ∈ wcel 2157  ∀wral 3089  ∃wrex 3090   class class class wbr 4843  Rel wrel 5317  ‘cfv 6101  (class class class)co 6878  ℂcc 10222   < clt 10363   − cmin 10556  ℤcz 11666  ℤ_≥cuz 11930  ℝ⁺crp 12074  abscabs 14315   ⇝ cli 14556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-opab 4906  df-xp 5318  df-rel 5319  df-clim 14560

This theorem is referenced by:  clim  14566  climcl  14571  climi  14582  climrlim2  14619  fclim  14625  climrecl  14655  climge0  14656  iserex  14728  caurcvg2  14749  caucvg  14750  iseralt  14756  fsumcvg3  14801  cvgcmpce  14888  climfsum  14890  climcnds  14921  trirecip  14933  ntrivcvgn0  14967  ovoliunlem1  23610  mbflimlem  23775  abelthlem5  24530  emcllem6  25079  lgamgulmlem4  25110  binomcxplemnn0  39330  binomcxplemnotnn0  39337  climf  40598  sumnnodd  40606  climf2  40642  climd  40648  clim2d  40649  climfv  40667  climuzlem  40719  climlimsup  40736  climlimsupcex  40745  climliminflimsupd  40777  climliminf  40782  liminflimsupclim  40783  ioodvbdlimc1lem2  40891  ioodvbdlimc2lem  40893  stirlinglem12  41045  fouriersw  41191