Theorem climrel 15463

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

Syntax hints:   ∧ wa 395   ∈ wcel 2099  ∀wral 3057  ∃wrex 3066   class class class wbr 5143  Rel wrel 5678  ‘cfv 6543  (class class class)co 7415  ℂcc 11131   < clt 11273   − cmin 11469  ℤcz 12583  ℤ_≥cuz 12847  ℝ⁺crp 13001  abscabs 15208   ⇝ cli 15455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952  df-ss 3962  df-opab 5206  df-xp 5679  df-rel 5680  df-clim 15459

This theorem is referenced by:  clim  15465  climcl  15470  climi  15481  climrlim2  15518  fclim  15524  climrecl  15554  climge0  15555  iserex  15630  caurcvg2  15651  caucvg  15652  iseralt  15658  fsumcvg3  15702  cvgcmpce  15791  climfsum  15793  climcnds  15824  trirecip  15836  ntrivcvgn0  15871  ovoliunlem1  25425  mbflimlem  25590  abelthlem5  26366  emcllem6  26927  lgamgulmlem4  26958  binomcxplemnn0  43777  binomcxplemnotnn0  43784  climf  45001  sumnnodd  45009  climf2  45045  climd  45051  clim2d  45052  climfv  45070  climuzlem  45122  climlimsup  45139  climlimsupcex  45148  climliminflimsupd  45180  climliminf  45185  liminflimsupclim  45186  xlimclimdm  45233  ioodvbdlimc1lem2  45311  ioodvbdlimc2lem  45313  stirlinglem12  45464  fouriersw  45610