Metamath Proof Explorer

Theorem climrel

Description: The limit relation is a relation. (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion climrel 
|- Rel ~~>

Proof

Step Hyp Ref Expression
1 df-clim 
 |-  ~~> = { <. 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 ) ) }
2 1 relopabiv 
 |-  Rel ~~>