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 = ( Base ` G )
	tsmscl.1	|- ( ph -> G e. CMnd )
	tsmscl.2	|- ( ph -> G e. TopSp )
	tsmscl.a	|- ( ph -> A e. V )
	tsmscl.f	|- ( ph -> F : A --> B )
	haustsms.j	|- J = ( TopOpen ` G )
	haustsms.h	|- ( ph -> J e. Haus )
Assertion	haustsms2	|- ( ph -> ( X e. ( G tsums F ) -> ( G tsums F ) = { X } ) )

Proof

Step	Hyp	Ref	Expression
1		tsmscl.b	|- B = ( Base ` G )
2		tsmscl.1	|- ( ph -> G e. CMnd )
3		tsmscl.2	|- ( ph -> G e. TopSp )
4		tsmscl.a	|- ( ph -> A e. V )
5		tsmscl.f	|- ( ph -> F : A --> B )
6		haustsms.j	|- J = ( TopOpen ` G )
7		haustsms.h	|- ( ph -> J e. Haus )
8		simpr	|- ( ( ph /\ X e. ( G tsums F ) ) -> X e. ( G tsums F ) )
9	1 2 3 4 5 6 7	haustsms	|- ( ph -> E* x x e. ( G tsums F ) )
10	9	adantr	|- ( ( ph /\ X e. ( G tsums F ) ) -> E* x x e. ( G tsums F ) )
11		eleq1	|- ( x = X -> ( x e. ( G tsums F ) <-> X e. ( G tsums F ) ) )
12	11	moi2	|- ( ( ( X e. ( G tsums F ) /\ E* x x e. ( G tsums F ) ) /\ ( x e. ( G tsums F ) /\ X e. ( G tsums F ) ) ) -> x = X )
13	12	ancom2s	|- ( ( ( X e. ( G tsums F ) /\ E* x x e. ( G tsums F ) ) /\ ( X e. ( G tsums F ) /\ x e. ( G tsums F ) ) ) -> x = X )
14	13	expr	|- ( ( ( X e. ( G tsums F ) /\ E* x x e. ( G tsums F ) ) /\ X e. ( G tsums F ) ) -> ( x e. ( G tsums F ) -> x = X ) )
15	8 10 8 14	syl21anc	|- ( ( ph /\ X e. ( G tsums F ) ) -> ( x e. ( G tsums F ) -> x = X ) )
16		velsn	|- ( x e. { X } <-> x = X )
17	15 16	imbitrrdi	|- ( ( ph /\ X e. ( G tsums F ) ) -> ( x e. ( G tsums F ) -> x e. { X } ) )
18	17	ssrdv	|- ( ( ph /\ X e. ( G tsums F ) ) -> ( G tsums F ) C_ { X } )
19		snssi	|- ( X e. ( G tsums F ) -> { X } C_ ( G tsums F ) )
20	19	adantl	|- ( ( ph /\ X e. ( G tsums F ) ) -> { X } C_ ( G tsums F ) )
21	18 20	eqssd	|- ( ( ph /\ X e. ( G tsums F ) ) -> ( G tsums F ) = { X } )
22	21	ex	|- ( ph -> ( X e. ( G tsums F ) -> ( G tsums F ) = { X } ) )