Theorem climrel 14424

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

Syntax hints:   ∧ wa 382   ∈ wcel 2145  ∀wral 3061  ∃wrex 3062   class class class wbr 4786  Rel wrel 5254  ‘cfv 6029  (class class class)co 6791  ℂcc 10134   < clt 10274   − cmin 10466  ℤcz 11577  ℤ_≥cuz 11886  ℝ⁺crp 12028  abscabs 14175   ⇝ cli 14416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-opab 4847  df-xp 5255  df-rel 5256  df-clim 14420

This theorem is referenced by:  clim  14426  climcl  14431  climi  14442  climrlim2  14479  fclim  14485  climrecl  14515  climge0  14516  iserex  14588  caurcvg2  14609  caucvg  14610  iseralt  14616  fsumcvg3  14661  cvgcmpce  14750  climfsum  14752  climcnds  14783  trirecip  14795  ntrivcvgn0  14830  ovoliunlem1  23483  mbflimlem  23647  abelthlem5  24402  emcllem6  24941  lgamgulmlem4  24972  binomcxplemnn0  39067  binomcxplemnotnn0  39074  climf  40365  sumnnodd  40373  climf2  40409  climd  40415  clim2d  40416  climfv  40434  climuzlem  40486  climlimsup  40503  climlimsupcex  40512  climliminflimsupd  40544  climliminf  40549  liminflimsupclim  40550  ioodvbdlimc1lem2  40658  ioodvbdlimc2lem  40660  stirlinglem12  40812  fouriersw  40958