MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  climrel Structured version   Unicode version

Theorem climrel 13072
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  j 
k  x  y  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-clim 13068 . 2  |-  ~~>  =  { <. f ,  y >.  |  ( y  e.  CC  /\  A. x  e.  RR+  E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j )
( ( f `  k )  e.  CC  /\  ( abs `  (
( f `  k
)  -  y ) )  <  x ) ) }
21relopabi 5063 1  |-  Rel  ~~>
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1758   A.wral 2795   E.wrex 2796   class class class wbr 4390   Rel wrel 4943   ` cfv 5516  (class class class)co 6190   CCcc 9381    < clt 9519    - cmin 9696   ZZcz 10747   ZZ>=cuz 10962   RR+crp 11092   abscabs 12825    ~~> cli 13064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-opab 4449  df-xp 4944  df-rel 4945  df-clim 13068
This theorem is referenced by:  clim  13074  climcl  13079  climi  13090  climrlim2  13127  fclim  13133  climrecl  13163  climge0  13164  iserex  13236  caurcvg2  13257  caucvg  13258  iseralt  13264  fsumcvg3  13308  cvgcmpce  13383  climfsum  13385  climcnds  13416  trirecip  13427  ovoliunlem1  21101  mbflimlem  21261  abelthlem5  22016  emcllem6  22510  lgamgulmlem4  27152  ntrivcvgn0  27547  stirlinglem12  30018
  Copyright terms: Public domain W3C validator