Theorem ulmcl

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

	Ref	Expression
Assertion	ulmcl	$$⊢F\underset{u}{⇝}\left(S\right)G\to G:S⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ulmscl	$$⊢F\underset{u}{⇝}\left(S\right)G\to S\in \mathrm{V}$$
2		ulmval	$$⊢S\in \mathrm{V}\to \left(F\underset{u}{⇝}\left(S\right)G\leftrightarrow \exists n\in \mathbb{Z}\left(F:{\mathbb{Z}}_{\ge n}⟶{ℂ}^S\wedge G:S⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\right)\right)$$
3	1 2	syl	$$⊢F\underset{u}{⇝}\left(S\right)G\to \left(F\underset{u}{⇝}\left(S\right)G\leftrightarrow \exists n\in \mathbb{Z}\left(F:{\mathbb{Z}}_{\ge n}⟶{ℂ}^S\wedge G:S⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\right)\right)$$
4	3	ibi	$$⊢F\underset{u}{⇝}\left(S\right)G\to \exists n\in \mathbb{Z}\left(F:{\mathbb{Z}}_{\ge n}⟶{ℂ}^S\wedge G:S⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\right)$$
5		simp2	$$⊢\left(F:{\mathbb{Z}}_{\ge n}⟶{ℂ}^S\wedge G:S⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\right)\to G:S⟶ℂ$$
6	5	rexlimivw	$$⊢\exists n\in \mathbb{Z}\left(F:{\mathbb{Z}}_{\ge n}⟶{ℂ}^S\wedge G:S⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\right)\to G:S⟶ℂ$$
7	4 6	syl	$$⊢F\underset{u}{⇝}\left(S\right)G\to G:S⟶ℂ$$