Theorem climrel 14851

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

Syntax hints:   ∧ wa 398   ∈ wcel 2114  ∀wral 3140  ∃wrex 3141   class class class wbr 5068  Rel wrel 5562  ‘cfv 6357  (class class class)co 7158  ℂcc 10537   < clt 10677   − cmin 10872  ℤcz 11984  ℤ_≥cuz 12246  ℝ⁺crp 12392  abscabs 14595   ⇝ cli 14843

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-opab 5131  df-xp 5563  df-rel 5564  df-clim 14847

This theorem is referenced by:  clim  14853  climcl  14858  climi  14869  climrlim2  14906  fclim  14912  climrecl  14942  climge0  14943  iserex  15015  caurcvg2  15036  caucvg  15037  iseralt  15043  fsumcvg3  15088  cvgcmpce  15175  climfsum  15177  climcnds  15208  trirecip  15220  ntrivcvgn0  15256  ovoliunlem1  24105  mbflimlem  24270  abelthlem5  25025  emcllem6  25580  lgamgulmlem4  25611  binomcxplemnn0  40688  binomcxplemnotnn0  40695  climf  41910  sumnnodd  41918  climf2  41954  climd  41960  clim2d  41961  climfv  41979  climuzlem  42031  climlimsup  42048  climlimsupcex  42057  climliminflimsupd  42089  climliminf  42094  liminflimsupclim  42095  xlimclimdm  42142  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  stirlinglem12  42377  fouriersw  42523