Metamath Proof Explorer


Theorem ulmscl

Description: Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Assertion ulmscl
|- ( F ( ~~>u ` S ) G -> S e. _V )

Proof

Step Hyp Ref Expression
1 df-br
 |-  ( F ( ~~>u ` S ) G <-> <. F , G >. e. ( ~~>u ` S ) )
2 elfvex
 |-  ( <. F , G >. e. ( ~~>u ` S ) -> S e. _V )
3 1 2 sylbi
 |-  ( F ( ~~>u ` S ) G -> S e. _V )