ulmi

Description: The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015)

	Ref	Expression
Hypotheses	ulm2.z	$⊢ Z = ℤ_{\geq M}$
	ulm2.m	$⊢ φ \to M \in ℤ$
	ulm2.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
	ulm2.b	$⊢ (φ \land (k \in Z \land z \in S)) \to F (k) (z) = B$
	ulm2.a	$⊢ (φ \land z \in S) \to G (z) = A$
	ulmi.u	$⊢ φ \to F \underset{u}{⇝} (S) G$
	ulmi.c	$⊢ φ \to C \in ℝ^{+}$
Assertion	ulmi	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < C$

Step	Hyp	Ref	Expression
1		ulm2.z	$⊢ Z = ℤ_{\geq M}$
2		ulm2.m	$⊢ φ \to M \in ℤ$
3		ulm2.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
4		ulm2.b	$⊢ (φ \land (k \in Z \land z \in S)) \to F (k) (z) = B$
5		ulm2.a	$⊢ (φ \land z \in S) \to G (z) = A$
6		ulmi.u	$⊢ φ \to F \underset{u}{⇝} (S) G$
7		ulmi.c	$⊢ φ \to C \in ℝ^{+}$
8		breq2	$⊢ x = C \to (\|B - A\| < x \leftrightarrow \|B - A\| < C)$
9	8	ralbidv	$⊢ x = C \to (\forall z \in S \|B - A\| < x \leftrightarrow \forall z \in S \|B - A\| < C)$
10	9	rexralbidv	$⊢ x = C \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < C)$
11		ulmcl	$⊢ F \underset{u}{⇝} (S) G \to G : S ⟶ ℂ$
12	6 11	syl	$⊢ φ \to G : S ⟶ ℂ$
13		ulmscl	$⊢ F \underset{u}{⇝} (S) G \to S \in V$
14	6 13	syl	$⊢ φ \to S \in V$
15	1 2 3 4 5 12 14	ulm2	$⊢ φ \to (F \underset{u}{⇝} (S) G \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x)$
16	6 15	mpbid	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < x$
17	10 16 7	rspcdva	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|B - A\| < C$

Metamath Proof Explorer