# Metamath Proof Explorer

## Theorem lmcls

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

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}$
lmcls.8 ${⊢}{\phi }\to {S}\subseteq {X}$
Assertion lmcls ${⊢}{\phi }\to {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)$

### 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 lmcls.8 ${⊢}{\phi }\to {S}\subseteq {X}$
7 2 1 3 lmbr2
8 4 7 mpbid ${⊢}{\phi }\to \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\wedge \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)\right)$
9 8 simp3d ${⊢}{\phi }\to \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)$
10 1 r19.2uz ${⊢}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)$
11 inelcm ${⊢}\left({F}\left({k}\right)\in {u}\wedge {F}\left({k}\right)\in {S}\right)\to {u}\cap {S}\ne \varnothing$
12 11 a1i ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left(\left({F}\left({k}\right)\in {u}\wedge {F}\left({k}\right)\in {S}\right)\to {u}\cap {S}\ne \varnothing \right)$
13 5 12 mpan2d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({F}\left({k}\right)\in {u}\to {u}\cap {S}\ne \varnothing \right)$
14 13 adantld ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\to {u}\cap {S}\ne \varnothing \right)$
15 14 rexlimdva ${⊢}{\phi }\to \left(\exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\to {u}\cap {S}\ne \varnothing \right)$
16 10 15 syl5 ${⊢}{\phi }\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\to {u}\cap {S}\ne \varnothing \right)$
17 16 imim2d ${⊢}{\phi }\to \left(\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)\to \left({P}\in {u}\to {u}\cap {S}\ne \varnothing \right)\right)$
18 17 ralimdv ${⊢}{\phi }\to \left(\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)\to \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to {u}\cap {S}\ne \varnothing \right)\right)$
19 9 18 mpd ${⊢}{\phi }\to \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to {u}\cap {S}\ne \varnothing \right)$
20 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
21 2 20 syl ${⊢}{\phi }\to {J}\in \mathrm{Top}$
22 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
23 2 22 syl ${⊢}{\phi }\to {X}=\bigcup {J}$
24 6 23 sseqtrd ${⊢}{\phi }\to {S}\subseteq \bigcup {J}$
25 lmcl
26 2 4 25 syl2anc ${⊢}{\phi }\to {P}\in {X}$
27 26 23 eleqtrd ${⊢}{\phi }\to {P}\in \bigcup {J}$
28 eqid ${⊢}\bigcup {J}=\bigcup {J}$
29 28 elcls ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq \bigcup {J}\wedge {P}\in \bigcup {J}\right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)↔\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to {u}\cap {S}\ne \varnothing \right)\right)$
30 21 24 27 29 syl3anc ${⊢}{\phi }\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)↔\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to {u}\cap {S}\ne \varnothing \right)\right)$
31 19 30 mpbird ${⊢}{\phi }\to {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)$