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 S 𝑝𝑚

Proof

Step Hyp Ref Expression
1 ulmf F u S G n F : n S
2 uzssz n
3 ovex S V
4 zex V
5 elpm2r S V V F : n S n F S 𝑝𝑚
6 3 4 5 mpanl12 F : n S n F S 𝑝𝑚
7 2 6 mpan2 F : n S F S 𝑝𝑚
8 7 rexlimivw n F : n S F S 𝑝𝑚
9 1 8 syl F u S G F S 𝑝𝑚