This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ulmcl

Description: Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Assertion ulmcl 
|- ( F ( ~~>u ` S ) G -> G : S --> CC )

Proof

Step Hyp Ref Expression
1 ulmscl 
 |-  ( F ( ~~>u ` S ) G -> S e. _V )
2 ulmval 
 |-  ( S e. _V -> ( F ( ~~>u ` S ) G <-> E. n e. ZZ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) )
3 1 2 syl 
 |-  ( F ( ~~>u ` S ) G -> ( F ( ~~>u ` S ) G <-> E. n e. ZZ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) )
4 3 ibi 
 |-  ( F ( ~~>u ` S ) G -> E. n e. ZZ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) )
5 simp2 
 |-  ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) -> G : S --> CC )
6 5 rexlimivw 
 |-  ( E. n e. ZZ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) -> G : S --> CC )
7 4 6 syl 
 |-  ( F ( ~~>u ` S ) G -> G : S --> CC )