This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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