Metamath Proof Explorer

Theorem ulmf

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

Ref Expression
Assertion ulmf 
|- ( F ( ~~>u ` S ) G -> E. n e. ZZ F : ( ZZ>= ` n ) --> ( CC ^m S ) )

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 simp1 
 |-  ( ( 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 ) -> F : ( ZZ>= ` n ) --> ( CC ^m S ) )
6 5 reximi 
 |-  ( 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 ) -> E. n e. ZZ F : ( ZZ>= ` n ) --> ( CC ^m S ) )
7 4 6 syl 
 |-  ( F ( ~~>u ` S ) G -> E. n e. ZZ F : ( ZZ>= ` n ) --> ( CC ^m S ) )