rlimcn1b

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 10-May-2016)

	Ref	Expression
Hypotheses	rlimcn1b.1	$⊢ (φ \land k \in A) \to B \in X$
	rlimcn1b.2	$⊢ φ \to C \in X$
	rlimcn1b.3	$⊢ φ \to (k \in A ⟼ B) \underset{ℝ}{⇝} C$
	rlimcn1b.4	$⊢ φ \to F : X ⟶ ℂ$
	rlimcn1b.5	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x)$
Assertion	rlimcn1b	$⊢ φ \to (k \in A ⟼ F (B)) \underset{ℝ}{⇝} F (C)$

Step	Hyp	Ref	Expression
1		rlimcn1b.1	$⊢ (φ \land k \in A) \to B \in X$
2		rlimcn1b.2	$⊢ φ \to C \in X$
3		rlimcn1b.3	$⊢ φ \to (k \in A ⟼ B) \underset{ℝ}{⇝} C$
4		rlimcn1b.4	$⊢ φ \to F : X ⟶ ℂ$
5		rlimcn1b.5	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in X (\|z - C\| < y \to \|F (z) - F (C)\| < x)$
6	4 1	cofmpt	$⊢ φ \to F \circ (k \in A ⟼ B) = (k \in A ⟼ F (B))$
7	1	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ X$
8	7 2 3 4 5	rlimcn1	$⊢ φ \to (F \circ (k \in A ⟼ B)) \underset{ℝ}{⇝} F (C)$
9	6 8	eqbrtrrd	$⊢ φ \to (k \in A ⟼ F (B)) \underset{ℝ}{⇝} F (C)$

Metamath Proof Explorer