Theorem tgpt1

Description: Hausdorff and T1 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypothesis	tgpt1.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion	tgpt1	⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Haus ↔ 𝐽 ∈ Fre ) )

Proof

Step	Hyp	Ref	Expression
1		tgpt1.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2		haust1	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Fre )
3		tgpgrp	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6	4 5	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
7	3 6	syl	⊢ ( 𝐺 ∈ TopGrp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
8	1 4	tgptopon	⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
9		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = ∪ 𝐽 )
10	8 9	syl	⊢ ( 𝐺 ∈ TopGrp → ( Base ‘ 𝐺 ) = ∪ 𝐽 )
11	7 10	eleqtrd	⊢ ( 𝐺 ∈ TopGrp → ( 0g ‘ 𝐺 ) ∈ ∪ 𝐽 )
12		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
13	12	t1sncld	⊢ ( ( 𝐽 ∈ Fre ∧ ( 0g ‘ 𝐺 ) ∈ ∪ 𝐽 ) → { ( 0g ‘ 𝐺 ) } ∈ ( Clsd ‘ 𝐽 ) )
14	13	expcom	⊢ ( ( 0g ‘ 𝐺 ) ∈ ∪ 𝐽 → ( 𝐽 ∈ Fre → { ( 0g ‘ 𝐺 ) } ∈ ( Clsd ‘ 𝐽 ) ) )
15	11 14	syl	⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Fre → { ( 0g ‘ 𝐺 ) } ∈ ( Clsd ‘ 𝐽 ) ) )
16	5 1	tgphaus	⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Haus ↔ { ( 0g ‘ 𝐺 ) } ∈ ( Clsd ‘ 𝐽 ) ) )
17	15 16	sylibrd	⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Fre → 𝐽 ∈ Haus ) )
18	2 17	impbid2	⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Haus ↔ 𝐽 ∈ Fre ) )