Metamath Proof Explorer

Theorem ulmf2

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

Ref Expression
Assertion ulmf2 
|- ( ( F Fn Z /\ F ( ~~>u ` S ) G ) -> F : Z --> ( CC ^m S ) )

Proof

Step Hyp Ref Expression
1 ulmpm 
 |-  ( F ( ~~>u ` S ) G -> F e. ( ( CC ^m S ) ^pm ZZ ) )
2 ovex 
 |-  ( CC ^m S ) e. _V
3 zex 
 |-  ZZ e. _V
4 2 3 elpm2 
 |-  ( F e. ( ( CC ^m S ) ^pm ZZ ) <-> ( F : dom F --> ( CC ^m S ) /\ dom F C_ ZZ ) )
5 4 simplbi 
 |-  ( F e. ( ( CC ^m S ) ^pm ZZ ) -> F : dom F --> ( CC ^m S ) )
6 1 5 syl 
 |-  ( F ( ~~>u ` S ) G -> F : dom F --> ( CC ^m S ) )
7 6 adantl 
 |-  ( ( F Fn Z /\ F ( ~~>u ` S ) G ) -> F : dom F --> ( CC ^m S ) )
8 fndm 
 |-  ( F Fn Z -> dom F = Z )
9 8 adantr 
 |-  ( ( F Fn Z /\ F ( ~~>u ` S ) G ) -> dom F = Z )
10 9 feq2d 
 |-  ( ( F Fn Z /\ F ( ~~>u ` S ) G ) -> ( F : dom F --> ( CC ^m S ) <-> F : Z --> ( CC ^m S ) ) )
11 7 10 mpbid 
 |-  ( ( F Fn Z /\ F ( ~~>u ` S ) G ) -> F : Z --> ( CC ^m S ) )