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	$⊢ Z = ℤ_{\geq M}$
		lmff.3	$⊢ φ \to J \in TopOn (X)$
		lmff.4	$⊢ φ \to M \in ℤ$
		lmcls.5	$⊢ φ \to F \underset{t}{⇝} (J) P$
		lmcls.7	$⊢ (φ \land k \in Z) \to F (k) \in S$
		lmcld.8	$⊢ φ \to S \in Clsd (J)$
	Assertion	lmcld	$⊢ φ \to P \in S$

Proof

Step	Hyp	Ref	Expression
1		lmff.1	$⊢ Z = ℤ_{\geq M}$
2		lmff.3	$⊢ φ \to J \in TopOn (X)$
3		lmff.4	$⊢ φ \to M \in ℤ$
4		lmcls.5	$⊢ φ \to F \underset{t}{⇝} (J) P$
5		lmcls.7	$⊢ (φ \land k \in Z) \to F (k) \in S$
6		lmcld.8	$⊢ φ \to S \in Clsd (J)$
7		eqid	$⊢ ⋃ J = ⋃ J$
8	7	cldss	$⊢ S \in Clsd (J) \to S \subseteq ⋃ J$
9	6 8	syl	$⊢ φ \to S \subseteq ⋃ J$
10		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
11	2 10	syl	$⊢ φ \to X = ⋃ J$
12	9 11	sseqtrrd	$⊢ φ \to S \subseteq X$
13	1 2 3 4 5 12	lmcls	$⊢ φ \to P \in cls (J) (S)$
14		cldcls	$⊢ S \in Clsd (J) \to cls (J) (S) = S$
15	6 14	syl	$⊢ φ \to cls (J) (S) = S$
16	13 15	eleqtrd	$⊢ φ \to P \in S$