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

Metamath Proof Explorer

Theorem lmcld

Description: Any convergent sequence of points in a closed subset of a topological space converges to a point in the set. (Contributed by Mario Carneiro, 30-Dec-2013)

Ref Expression
Hypotheses lmff.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
lmff.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
lmff.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
lmcls.5 ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
lmcls.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
lmcld.8 ⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
Assertion lmcld ( 𝜑 → 𝑃 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lmff.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 lmff.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 lmff.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 lmcls.5 ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
5 lmcls.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
6 lmcld.8 ⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
7 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
8 7 cldss ⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → 𝑆 ⊆ ∪ 𝐽 )
9 6 8 syl ⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
10 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
11 2 10 syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
12 9 11 sseqtrrd ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
13 1 2 3 4 5 12 lmcls ⊢ ( 𝜑 → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
14 cldcls ⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 )
15 6 14 syl ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 )
16 13 15 eleqtrd ⊢ ( 𝜑 → 𝑃 ∈ 𝑆 )