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 ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
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 ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐺 ‘ 𝑃 ) )