# Metamath Proof Explorer

## Theorem haustsms2

Description: In a Hausdorff topological group, a sum has at most one limit point. (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypotheses tsmscl.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
tsmscl.1 ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
tsmscl.2 ${⊢}{\phi }\to {G}\in \mathrm{TopSp}$
tsmscl.a ${⊢}{\phi }\to {A}\in {V}$
tsmscl.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
haustsms.j ${⊢}{J}=\mathrm{TopOpen}\left({G}\right)$
haustsms.h ${⊢}{\phi }\to {J}\in \mathrm{Haus}$
Assertion haustsms2 ${⊢}{\phi }\to \left({X}\in \left({G}\mathrm{tsums}{F}\right)\to {G}\mathrm{tsums}{F}=\left\{{X}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 tsmscl.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 tsmscl.1 ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
3 tsmscl.2 ${⊢}{\phi }\to {G}\in \mathrm{TopSp}$
4 tsmscl.a ${⊢}{\phi }\to {A}\in {V}$
5 tsmscl.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
6 haustsms.j ${⊢}{J}=\mathrm{TopOpen}\left({G}\right)$
7 haustsms.h ${⊢}{\phi }\to {J}\in \mathrm{Haus}$
8 simpr ${⊢}\left({\phi }\wedge {X}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {X}\in \left({G}\mathrm{tsums}{F}\right)$
9 1 2 3 4 5 6 7 haustsms ${⊢}{\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{x}\in \left({G}\mathrm{tsums}{F}\right)$
10 9 adantr ${⊢}\left({\phi }\wedge {X}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{x}\in \left({G}\mathrm{tsums}{F}\right)$
11 eleq1 ${⊢}{x}={X}\to \left({x}\in \left({G}\mathrm{tsums}{F}\right)↔{X}\in \left({G}\mathrm{tsums}{F}\right)\right)$
12 11 moi2 ${⊢}\left(\left({X}\in \left({G}\mathrm{tsums}{F}\right)\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{x}\in \left({G}\mathrm{tsums}{F}\right)\right)\wedge \left({x}\in \left({G}\mathrm{tsums}{F}\right)\wedge {X}\in \left({G}\mathrm{tsums}{F}\right)\right)\right)\to {x}={X}$
13 12 ancom2s ${⊢}\left(\left({X}\in \left({G}\mathrm{tsums}{F}\right)\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{x}\in \left({G}\mathrm{tsums}{F}\right)\right)\wedge \left({X}\in \left({G}\mathrm{tsums}{F}\right)\wedge {x}\in \left({G}\mathrm{tsums}{F}\right)\right)\right)\to {x}={X}$
14 13 expr ${⊢}\left(\left({X}\in \left({G}\mathrm{tsums}{F}\right)\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{x}\in \left({G}\mathrm{tsums}{F}\right)\right)\wedge {X}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left({x}\in \left({G}\mathrm{tsums}{F}\right)\to {x}={X}\right)$
15 8 10 8 14 syl21anc ${⊢}\left({\phi }\wedge {X}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left({x}\in \left({G}\mathrm{tsums}{F}\right)\to {x}={X}\right)$
16 velsn ${⊢}{x}\in \left\{{X}\right\}↔{x}={X}$
17 15 16 syl6ibr ${⊢}\left({\phi }\wedge {X}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left({x}\in \left({G}\mathrm{tsums}{F}\right)\to {x}\in \left\{{X}\right\}\right)$
18 17 ssrdv ${⊢}\left({\phi }\wedge {X}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\mathrm{tsums}{F}\subseteq \left\{{X}\right\}$
19 snssi ${⊢}{X}\in \left({G}\mathrm{tsums}{F}\right)\to \left\{{X}\right\}\subseteq {G}\mathrm{tsums}{F}$
20 19 adantl ${⊢}\left({\phi }\wedge {X}\in \left({G}\mathrm{tsums}{F}\right)\right)\to \left\{{X}\right\}\subseteq {G}\mathrm{tsums}{F}$
21 18 20 eqssd ${⊢}\left({\phi }\wedge {X}\in \left({G}\mathrm{tsums}{F}\right)\right)\to {G}\mathrm{tsums}{F}=\left\{{X}\right\}$
22 21 ex ${⊢}{\phi }\to \left({X}\in \left({G}\mathrm{tsums}{F}\right)\to {G}\mathrm{tsums}{F}=\left\{{X}\right\}\right)$