Theorem climcncf

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Hypotheses	climcncf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climcncf.2	$$⊢\phi \to M\in \mathbb{Z}$$
	climcncf.4	$$⊢\phi \to F:A\underset{cn}{⟶}B$$
	climcncf.5	$$⊢\phi \to G:Z⟶A$$
	climcncf.6	$$⊢\phi \to G⇝D$$
	climcncf.7	$$⊢\phi \to D\in A$$
Assertion	climcncf	$$⊢\phi \to \left(F\circ G\right)⇝F\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		climcncf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climcncf.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climcncf.4	$$⊢\phi \to F:A\underset{cn}{⟶}B$$
4		climcncf.5	$$⊢\phi \to G:Z⟶A$$
5		climcncf.6	$$⊢\phi \to G⇝D$$
6		climcncf.7	$$⊢\phi \to D\in A$$
7		cncff	$$⊢F:A\underset{cn}{⟶}B\to F:A⟶B$$
8	3 7	syl	$$⊢\phi \to F:A⟶B$$
9	8	ffvelcdmda	$$⊢\left(\phi \wedge z\in A\right)\to F\left(z\right)\in B$$
10		cncfrss2	$$⊢F:A\underset{cn}{⟶}B\to B\subseteq ℂ$$
11	3 10	syl	$$⊢\phi \to B\subseteq ℂ$$
12	11	sselda	$$⊢\left(\phi \wedge F\left(z\right)\in B\right)\to F\left(z\right)\in ℂ$$
13	9 12	syldan	$$⊢\left(\phi \wedge z\in A\right)\to F\left(z\right)\in ℂ$$
14	1	fvexi	$$⊢Z\in \mathrm{V}$$
15		fex	$$⊢\left(G:Z⟶A\wedge Z\in \mathrm{V}\right)\to G\in \mathrm{V}$$
16	4 14 15	sylancl	$$⊢\phi \to G\in \mathrm{V}$$
17		coexg	$$⊢\left(F:A\underset{cn}{⟶}B\wedge G\in \mathrm{V}\right)\to F\circ G\in \mathrm{V}$$
18	3 16 17	syl2anc	$$⊢\phi \to F\circ G\in \mathrm{V}$$
19		cncfi	$$⊢\left(F:A\underset{cn}{⟶}B\wedge D\in A\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in A\left(\left|z-D\right|<y\to \left|F\left(z\right)-F\left(D\right)\right|<x\right)$$
20	19	3expia	$$⊢\left(F:A\underset{cn}{⟶}B\wedge D\in A\right)\to \left(x\in {ℝ}^{+}\to \exists y\in {ℝ}^{+}\forall z\in A\left(\left|z-D\right|<y\to \left|F\left(z\right)-F\left(D\right)\right|<x\right)\right)$$
21	3 6 20	syl2anc	$$⊢\phi \to \left(x\in {ℝ}^{+}\to \exists y\in {ℝ}^{+}\forall z\in A\left(\left|z-D\right|<y\to \left|F\left(z\right)-F\left(D\right)\right|<x\right)\right)$$
22	21	imp	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in A\left(\left|z-D\right|<y\to \left|F\left(z\right)-F\left(D\right)\right|<x\right)$$
23	4	ffvelcdmda	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in A$$
24		fvco3	$$⊢\left(G:Z⟶A\wedge k\in Z\right)\to \left(F\circ G\right)\left(k\right)=F\left(G\left(k\right)\right)$$
25	4 24	sylan	$$⊢\left(\phi \wedge k\in Z\right)\to \left(F\circ G\right)\left(k\right)=F\left(G\left(k\right)\right)$$
26	1 2 6 13 5 18 22 23 25	climcn1	$$⊢\phi \to \left(F\circ G\right)⇝F\left(D\right)$$