ulmpm

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

		Ref	Expression
	Assertion	ulmpm	$⊢ F \underset{u}{⇝} (S) G \to F \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ)$

Step	Hyp	Ref	Expression
1		ulmf	$⊢ F \underset{u}{⇝} (S) G \to \exists n \in ℤ F : ℤ_{\geq n} ⟶ ℂ^{S}$
2		uzssz	$⊢ ℤ_{\geq n} \subseteq ℤ$
3		ovex	$⊢ ℂ^{S} \in V$
4		zex	$⊢ ℤ \in V$
5		elpm2r	$⊢ ((ℂ^{S} \in V \land ℤ \in V) \land (F : ℤ_{\geq n} ⟶ ℂ^{S} \land ℤ_{\geq n} \subseteq ℤ)) \to F \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ)$
6	3 4 5	mpanl12	$⊢ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land ℤ_{\geq n} \subseteq ℤ) \to F \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ)$
7	2 6	mpan2	$⊢ F : ℤ_{\geq n} ⟶ ℂ^{S} \to F \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ)$
8	7	rexlimivw	$⊢ \exists n \in ℤ F : ℤ_{\geq n} ⟶ ℂ^{S} \to F \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ)$
9	1 8	syl	$⊢ F \underset{u}{⇝} (S) G \to F \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ)$

Metamath Proof Explorer