This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 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 } ) )