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	relopabi	|- Rel ~~>r