# 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}={ℤ}_{\ge {M}}$
lmff.3 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
lmff.4 ${⊢}{\phi }\to {M}\in ℤ$
lmcls.5
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}={ℤ}_{\ge {M}}$
2 lmff.3 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
3 lmff.4 ${⊢}{\phi }\to {M}\in ℤ$
4 lmcls.5
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}$