Metamath Proof Explorer

Theorem ulmpm

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

Ref Expression
Assertion ulmpm 
|- ( F ( ~~>u ` S ) G -> F e. ( ( CC ^m S ) ^pm ZZ ) )

Proof

Step Hyp Ref Expression
1 ulmf 
 |-  ( F ( ~~>u ` S ) G -> E. n e. ZZ F : ( ZZ>= ` n ) --> ( CC ^m S ) )
2 uzssz 
 |-  ( ZZ>= ` n ) C_ ZZ
3 ovex 
 |-  ( CC ^m S ) e. _V
4 zex 
 |-  ZZ e. _V
5 elpm2r 
 |-  ( ( ( ( CC ^m S ) e. _V /\ ZZ e. _V ) /\ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ ( ZZ>= ` n ) C_ ZZ ) ) -> F e. ( ( CC ^m S ) ^pm ZZ ) )
6 3 4 5 mpanl12 
 |-  ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ ( ZZ>= ` n ) C_ ZZ ) -> F e. ( ( CC ^m S ) ^pm ZZ ) )
7 2 6 mpan2 
 |-  ( F : ( ZZ>= ` n ) --> ( CC ^m S ) -> F e. ( ( CC ^m S ) ^pm ZZ ) )
8 7 rexlimivw 
 |-  ( E. n e. ZZ F : ( ZZ>= ` n ) --> ( CC ^m S ) -> F e. ( ( CC ^m S ) ^pm ZZ ) )
9 1 8 syl 
 |-  ( F ( ~~>u ` S ) G -> F e. ( ( CC ^m S ) ^pm ZZ ) )