Metamath Proof Explorer


Theorem rlimrel

Description: The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014)

Ref Expression
Assertion rlimrel
|- Rel ~~>r

Proof

Step Hyp Ref Expression
1 df-rlim
 |-  ~~>r = { <. f , x >. | ( ( f e. ( CC ^pm RR ) /\ x e. CC ) /\ A. y e. RR+ E. z e. RR A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y ) ) }
2 1 relopabiv
 |-  Rel ~~>r