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 𝐹 ) = { 𝑋 } ) )