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 ⊢ J = TopOpen ⁡ G
Assertion tgpt1 ⊢ G ∈ TopGrp → J ∈ Haus ↔ J ∈ Fre

Proof

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