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 ⊢ φ → F ⇝t ⁡ J P
lmcn.4 ⊢ φ → G ∈ J Cn K
Assertion lmcn ⊢ φ → G ∘ F ⇝t ⁡ K G ⁡ P

Proof

Step Hyp Ref Expression
1 lmcnp.3 ⊢ φ → F ⇝t ⁡ J P
2 lmcn.4 ⊢ φ → G ∈ J Cn K
3 cntop1 ⊢ G ∈ J Cn K → J ∈ Top
4 2 3 syl ⊢ φ → J ∈ Top
5 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
6 4 5 sylib ⊢ φ → J ∈ TopOn ⁡ ⋃ J
7 lmcl ⊢ J ∈ TopOn ⁡ ⋃ J ∧ F ⇝t ⁡ J P → P ∈ ⋃ J
8 6 1 7 syl2anc ⊢ φ → P ∈ ⋃ J
9 eqid ⊢ ⋃ J = ⋃ J
10 9 cncnpi ⊢ G ∈ J Cn K ∧ P ∈ ⋃ J → G ∈ J CnP K ⁡ P
11 2 8 10 syl2anc ⊢ φ → G ∈ J CnP K ⁡ P
12 1 11 lmcnp ⊢ φ → G ∘ F ⇝t ⁡ K G ⁡ P