# Metamath Proof Explorer

## Theorem ulmcl

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

Ref Expression
Assertion ulmcl

### Proof

Step Hyp Ref Expression
1 ulmscl
2 ulmval
3 1 2 syl
4 3 ibi
5 simp2 ${⊢}\left({F}:{ℤ}_{\ge {n}}⟶{ℂ}^{{S}}\wedge {G}:{S}⟶ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right|<{x}\right)\to {G}:{S}⟶ℂ$
6 5 rexlimivw ${⊢}\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\left({F}:{ℤ}_{\ge {n}}⟶{ℂ}^{{S}}\wedge {G}:{S}⟶ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right|<{x}\right)\to {G}:{S}⟶ℂ$
7 4 6 syl