Metamath Proof Explorer


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 ) )