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 e. _V |-> { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } )
2 1 relmptopab
 |-  Rel ( ~~>u ` S )