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 )