Theorem ulmf

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

	Ref	Expression
Assertion	ulmf	$$⊢F\underset{u}{⇝}\left(S\right)G\to \exists n\in \mathbb{Z}F:{\mathbb{Z}}_{\ge n}⟶{ℂ}^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		simp1	$$⊢\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 F:{\mathbb{Z}}_{\ge n}⟶{ℂ}^S$$
6	5	reximi	$$⊢\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 \exists n\in \mathbb{Z}F:{\mathbb{Z}}_{\ge n}⟶{ℂ}^S$$
7	4 6	syl	$$⊢F\underset{u}{⇝}\left(S\right)G\to \exists n\in \mathbb{Z}F:{\mathbb{Z}}_{\ge n}⟶{ℂ}^S$$