haustsms2

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

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

Metamath Proof Explorer