ulmf2

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

		Ref	Expression
	Assertion	ulmf2	$⊢ (F Fn Z \land F \underset{u}{⇝} (S) G) \to F : Z ⟶ ℂ^{S}$

Step	Hyp	Ref	Expression
1		ulmpm	$⊢ F \underset{u}{⇝} (S) G \to F \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ)$
2		ovex	$⊢ ℂ^{S} \in V$
3		zex	$⊢ ℤ \in V$
4	2 3	elpm2	$⊢ F \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \leftrightarrow (F : dom F ⟶ ℂ^{S} \land dom F \subseteq ℤ)$
5	4	simplbi	$⊢ F \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \to F : dom F ⟶ ℂ^{S}$
6	1 5	syl	$⊢ F \underset{u}{⇝} (S) G \to F : dom F ⟶ ℂ^{S}$
7	6	adantl	$⊢ (F Fn Z \land F \underset{u}{⇝} (S) G) \to F : dom F ⟶ ℂ^{S}$
8		fndm	$⊢ F Fn Z \to dom F = Z$
9	8	adantr	$⊢ (F Fn Z \land F \underset{u}{⇝} (S) G) \to dom F = Z$
10	9	feq2d	$⊢ (F Fn Z \land F \underset{u}{⇝} (S) G) \to (F : dom F ⟶ ℂ^{S} \leftrightarrow F : Z ⟶ ℂ^{S})$
11	7 10	mpbid	$⊢ (F Fn Z \land F \underset{u}{⇝} (S) G) \to F : Z ⟶ ℂ^{S}$

Metamath Proof Explorer