ulmf

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

		Ref	Expression
	Assertion	ulmf	$⊢ F \underset{u}{⇝} (S) G \to \exists n \in ℤ F : ℤ_{\geq n} ⟶ ℂ^{S}$

Step	Hyp	Ref	Expression
1		ulmscl	$⊢ F \underset{u}{⇝} (S) G \to S \in V$
2		ulmval	$⊢ S \in V \to (F \underset{u}{⇝} (S) G \leftrightarrow \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$
3	1 2	syl	$⊢ F \underset{u}{⇝} (S) G \to (F \underset{u}{⇝} (S) G \leftrightarrow \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$
4	3	ibi	$⊢ F \underset{u}{⇝} (S) G \to \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x)$
5		simp1	$⊢ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \to F : ℤ_{\geq n} ⟶ ℂ^{S}$
6	5	reximi	$⊢ \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \to \exists n \in ℤ F : ℤ_{\geq n} ⟶ ℂ^{S}$
7	4 6	syl	$⊢ F \underset{u}{⇝} (S) G \to \exists n \in ℤ F : ℤ_{\geq n} ⟶ ℂ^{S}$

Metamath Proof Explorer