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 e. TopGrp -> ( J e. Haus <-> J e. Fre ) )

Proof

Step Hyp Ref Expression
1 tgpt1.j
 |-  J = ( TopOpen ` G )
2 haust1
 |-  ( J e. Haus -> J e. Fre )
3 tgpgrp
 |-  ( G e. TopGrp -> G e. Grp )
4 eqid
 |-  ( Base ` G ) = ( Base ` G )
5 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
6 4 5 grpidcl
 |-  ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) )
7 3 6 syl
 |-  ( G e. TopGrp -> ( 0g ` G ) e. ( Base ` G ) )
8 1 4 tgptopon
 |-  ( G e. TopGrp -> J e. ( TopOn ` ( Base ` G ) ) )
9 toponuni
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> ( Base ` G ) = U. J )
10 8 9 syl
 |-  ( G e. TopGrp -> ( Base ` G ) = U. J )
11 7 10 eleqtrd
 |-  ( G e. TopGrp -> ( 0g ` G ) e. U. J )
12 eqid
 |-  U. J = U. J
13 12 t1sncld
 |-  ( ( J e. Fre /\ ( 0g ` G ) e. U. J ) -> { ( 0g ` G ) } e. ( Clsd ` J ) )
14 13 expcom
 |-  ( ( 0g ` G ) e. U. J -> ( J e. Fre -> { ( 0g ` G ) } e. ( Clsd ` J ) ) )
15 11 14 syl
 |-  ( G e. TopGrp -> ( J e. Fre -> { ( 0g ` G ) } e. ( Clsd ` J ) ) )
16 5 1 tgphaus
 |-  ( G e. TopGrp -> ( J e. Haus <-> { ( 0g ` G ) } e. ( Clsd ` J ) ) )
17 15 16 sylibrd
 |-  ( G e. TopGrp -> ( J e. Fre -> J e. Haus ) )
18 2 17 impbid2
 |-  ( G e. TopGrp -> ( J e. Haus <-> J e. Fre ) )