Theorem rlimcn1b

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

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

Proof

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