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	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
	lmcn.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	lmcn	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐺 ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		lmcnp.3	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
2		lmcn.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
3		cntop1	⊢ ( 𝐺 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
4	2 3	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
5		toptopon2	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
6	4 5	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
7		lmcl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → 𝑃 ∈ ∪ 𝐽 )
8	6 1 7	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ ∪ 𝐽 )
9		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
10	9	cncnpi	⊢ ( ( 𝐺 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑃 ∈ ∪ 𝐽 ) → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
11	2 8 10	syl2anc	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
12	1 11	lmcnp	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐺 ‘ 𝑃 ) )