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	|- ( ph -> F ( ~~>t ` J ) P )
	lmcn.4	|- ( ph -> G e. ( J Cn K ) )
Assertion	lmcn	|- ( ph -> ( G o. F ) ( ~~>t ` K ) ( G ` P ) )

Proof

Step	Hyp	Ref	Expression
1		lmcnp.3	|- ( ph -> F ( ~~>t ` J ) P )
2		lmcn.4	|- ( ph -> G e. ( J Cn K ) )
3		cntop1	|- ( G e. ( J Cn K ) -> J e. Top )
4	2 3	syl	|- ( ph -> J e. Top )
5		toptopon2	|- ( J e. Top <-> J e. ( TopOn ` U. J ) )
6	4 5	sylib	|- ( ph -> J e. ( TopOn ` U. J ) )
7		lmcl	|- ( ( J e. ( TopOn ` U. J ) /\ F ( ~~>t ` J ) P ) -> P e. U. J )
8	6 1 7	syl2anc	|- ( ph -> P e. U. J )
9		eqid	|- U. J = U. J
10	9	cncnpi	|- ( ( G e. ( J Cn K ) /\ P e. U. J ) -> G e. ( ( J CnP K ) ` P ) )
11	2 8 10	syl2anc	|- ( ph -> G e. ( ( J CnP K ) ` P ) )
12	1 11	lmcnp	|- ( ph -> ( G o. F ) ( ~~>t ` K ) ( G ` P ) )