rlimcn2

Description: Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014)

	Ref	Expression
Hypotheses	rlimcn2.1a	$⊢ (φ \land z \in A) \to B \in X$
	rlimcn2.1b	$⊢ (φ \land z \in A) \to C \in Y$
	rlimcn2.2a	$⊢ φ \to R \in X$
	rlimcn2.2b	$⊢ φ \to S \in Y$
	rlimcn2.3a	$⊢ φ \to (z \in A ⟼ B) \underset{ℝ}{⇝} R$
	rlimcn2.3b	$⊢ φ \to (z \in A ⟼ C) \underset{ℝ}{⇝} S$
	rlimcn2.4	$⊢ φ \to F : X \times Y ⟶ ℂ$
	rlimcn2.5	$⊢ (φ \land x \in ℝ^{+}) \to \exists r \in ℝ^{+} \exists s \in ℝ^{+} \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)$
Assertion	rlimcn2	$⊢ φ \to (z \in A ⟼ B F C) \underset{ℝ}{⇝} (R F S)$

Step	Hyp	Ref	Expression
1		rlimcn2.1a	$⊢ (φ \land z \in A) \to B \in X$
2		rlimcn2.1b	$⊢ (φ \land z \in A) \to C \in Y$
3		rlimcn2.2a	$⊢ φ \to R \in X$
4		rlimcn2.2b	$⊢ φ \to S \in Y$
5		rlimcn2.3a	$⊢ φ \to (z \in A ⟼ B) \underset{ℝ}{⇝} R$
6		rlimcn2.3b	$⊢ φ \to (z \in A ⟼ C) \underset{ℝ}{⇝} S$
7		rlimcn2.4	$⊢ φ \to F : X \times Y ⟶ ℂ$
8		rlimcn2.5	$⊢ (φ \land x \in ℝ^{+}) \to \exists r \in ℝ^{+} \exists s \in ℝ^{+} \forall u \in X \forall v \in Y ((\|u - R\| < r \land \|v - S\| < s) \to \|(u F v) - (R F S)\| < x)$
9	7	adantr	$⊢ (φ \land z \in A) \to F : X \times Y ⟶ ℂ$
10	9 1 2	fovcdmd	$⊢ (φ \land z \in A) \to B F C \in ℂ$
11	7 3 4	fovcdmd	$⊢ φ \to R F S \in ℂ$
12	1 2 10 11 5 6 8	rlimcn3	$⊢ φ \to (z \in A ⟼ B F C) \underset{ℝ}{⇝} (R F S)$

Metamath Proof Explorer