Metamath Proof Explorer


Theorem ulmrel

Description: The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Assertion ulmrel Rel u S

Proof

Step Hyp Ref Expression
1 df-ulm u = s V f y | n f : n s y : s x + j n k j z s f k z y z < x
2 1 relmptopab Rel u S