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 ⊢ φ → G ∈ CMnd
tsmscl.2 ⊢ φ → G ∈ TopSp
tsmscl.a ⊢ φ → A ∈ V
tsmscl.f ⊢ φ → F : A ⟶ B
haustsms.j ⊢ J = TopOpen ⁡ G
haustsms.h ⊢ φ → J ∈ Haus
Assertion haustsms2 ⊢ φ → X ∈ G tsums F → G tsums F = X

Proof

Step Hyp Ref Expression
1 tsmscl.b ⊢ B = Base G
2 tsmscl.1 ⊢ φ → G ∈ CMnd
3 tsmscl.2 ⊢ φ → G ∈ TopSp
4 tsmscl.a ⊢ φ → A ∈ V
5 tsmscl.f ⊢ φ → F : A ⟶ B
6 haustsms.j ⊢ J = TopOpen ⁡ G
7 haustsms.h ⊢ φ → J ∈ Haus
8 simpr ⊢ φ ∧ X ∈ G tsums F → X ∈ G tsums F
9 1 2 3 4 5 6 7 haustsms ⊢ φ → ∃* x x ∈ G tsums F
10 9 adantr ⊢ φ ∧ X ∈ G tsums F → ∃* x x ∈ G tsums F
11 eleq1 ⊢ x = X → x ∈ G tsums F ↔ X ∈ G tsums F
12 11 moi2 ⊢ X ∈ G tsums F ∧ ∃* x x ∈ G tsums F ∧ x ∈ G tsums F ∧ X ∈ G tsums F → x = X
13 12 ancom2s ⊢ X ∈ G tsums F ∧ ∃* x x ∈ G tsums F ∧ X ∈ G tsums F ∧ x ∈ G tsums F → x = X
14 13 expr ⊢ X ∈ G tsums F ∧ ∃* x x ∈ G tsums F ∧ X ∈ G tsums F → x ∈ G tsums F → x = X
15 8 10 8 14 syl21anc ⊢ φ ∧ X ∈ G tsums F → x ∈ G tsums F → x = X
16 velsn ⊢ x ∈ X ↔ x = X
17 15 16 imbitrrdi ⊢ φ ∧ X ∈ G tsums F → x ∈ G tsums F → x ∈ X
18 17 ssrdv ⊢ φ ∧ X ∈ G tsums F → G tsums F ⊆ X
19 snssi ⊢ X ∈ G tsums F → X ⊆ G tsums F
20 19 adantl ⊢ φ ∧ X ∈ G tsums F → X ⊆ G tsums F
21 18 20 eqssd ⊢ φ ∧ X ∈ G tsums F → G tsums F = X
22 21 ex ⊢ φ → X ∈ G tsums F → G tsums F = X