Metamath Proof Explorer


Theorem rlimrel

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

Ref Expression
Assertion rlimrel Rel

Proof

Step Hyp Ref Expression
1 df-rlim = f x | f 𝑝𝑚 x y + z w dom f z w f w x < y
2 1 relopabiv Rel