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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmscl.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmscl.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
tsmscl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmscl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
haustsms.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
haustsms.h ⊢ ( 𝜑 → 𝐽 ∈ Haus )
Assertion haustsms2 ( 𝜑 → ( 𝑋 ∈ ( 𝐺 tsums 𝐹 ) → ( 𝐺 tsums 𝐹 ) = { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 tsmscl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmscl.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
3 tsmscl.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
4 tsmscl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 tsmscl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6 haustsms.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
7 haustsms.h ⊢ ( 𝜑 → 𝐽 ∈ Haus )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
9 1 2 3 4 5 6 7 haustsms ⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ ( 𝐺 tsums 𝐹 ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) → ∃* 𝑥 𝑥 ∈ ( 𝐺 tsums 𝐹 ) )
11 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) )
12 11 moi2 ⊢ ( ( ( 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ∧ ∃* 𝑥 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) ∧ ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ∧ 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) ) → 𝑥 = 𝑋 )
13 12 ancom2s ⊢ ( ( ( 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ∧ ∃* 𝑥 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) ∧ ( 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) ) → 𝑥 = 𝑋 )
14 13 expr ⊢ ( ( ( 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ∧ ∃* 𝑥 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) ∧ 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) → 𝑥 = 𝑋 ) )
15 8 10 8 14 syl21anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) → 𝑥 = 𝑋 ) )
16 velsn ⊢ ( 𝑥 ∈ { 𝑋 } ↔ 𝑥 = 𝑋 )
17 15 16 imbitrrdi ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) → 𝑥 ∈ { 𝑋 } ) )
18 17 ssrdv ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) → ( 𝐺 tsums 𝐹 ) ⊆ { 𝑋 } )
19 snssi ⊢ ( 𝑋 ∈ ( 𝐺 tsums 𝐹 ) → { 𝑋 } ⊆ ( 𝐺 tsums 𝐹 ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) → { 𝑋 } ⊆ ( 𝐺 tsums 𝐹 ) )
21 18 20 eqssd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) → ( 𝐺 tsums 𝐹 ) = { 𝑋 } )
22 21 ex ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐺 tsums 𝐹 ) → ( 𝐺 tsums 𝐹 ) = { 𝑋 } ) )