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