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	⊢ ( 𝜑 → 𝑃 ∈ 𝑆 )