This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )