Theorem lmcn

Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014)

	Ref	Expression
Hypotheses	lmcnp.3	$$⊢\phi \to F\underset{t}{⇝}\left(J\right)P$$
	lmcn.4	$$⊢\phi \to G\in \left(J\mathrm{Cn}K\right)$$
Assertion	lmcn	$$⊢\phi \to \left(G\circ F\right)\underset{t}{⇝}\left(K\right)G\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmcnp.3	$$⊢\phi \to F\underset{t}{⇝}\left(J\right)P$$
2		lmcn.4	$$⊢\phi \to G\in \left(J\mathrm{Cn}K\right)$$
3		cntop1	$$⊢G\in \left(J\mathrm{Cn}K\right)\to J\in \mathrm{Top}$$
4	2 3	syl	$$⊢\phi \to J\in \mathrm{Top}$$
5		toptopon2	$$⊢J\in \mathrm{Top}\leftrightarrow J\in \mathrm{TopOn}\left(\bigcup J\right)$$
6	4 5	sylib	$$⊢\phi \to J\in \mathrm{TopOn}\left(\bigcup J\right)$$
7		lmcl	$$⊢\left(J\in \mathrm{TopOn}\left(\bigcup J\right)\wedge F\underset{t}{⇝}\left(J\right)P\right)\to P\in \bigcup J$$
8	6 1 7	syl2anc	$$⊢\phi \to P\in \bigcup J$$
9		eqid	$$⊢\bigcup J=\bigcup J$$
10	9	cncnpi	$$⊢\left(G\in \left(J\mathrm{Cn}K\right)\wedge P\in \bigcup J\right)\to G\in \left(J\mathrm{CnP}K\right)\left(P\right)$$
11	2 8 10	syl2anc	$$⊢\phi \to G\in \left(J\mathrm{CnP}K\right)\left(P\right)$$
12	1 11	lmcnp	$$⊢\phi \to \left(G\circ F\right)\underset{t}{⇝}\left(K\right)G\left(P\right)$$