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={\mathbb{Z}}_{\ge M}$$
	lmff.3	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	lmff.4	$$⊢\phi \to M\in \mathbb{Z}$$
	lmcls.5	$$⊢\phi \to F\underset{t}{⇝}\left(J\right)P$$
	lmcls.7	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in S$$
	lmcld.8	$$⊢\phi \to S\in \mathrm{Clsd}\left(J\right)$$
Assertion	lmcld	$$⊢\phi \to P\in S$$

Proof

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