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 \in TopGrp \to (J \in Haus \leftrightarrow J \in Fre)$

Step	Hyp	Ref	Expression
1		tgpt1.j	$⊢ J = TopOpen (G)$
2		haust1	$⊢ J \in Haus \to J \in Fre$
3		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
4		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5		eqid	$⊢ 0_{G} = 0_{G}$
6	4 5	grpidcl	$⊢ G \in Grp \to 0_{G} \in {Base}_{G}$
7	3 6	syl	$⊢ G \in TopGrp \to 0_{G} \in {Base}_{G}$
8	1 4	tgptopon	$⊢ G \in TopGrp \to J \in TopOn ({Base}_{G})$
9		toponuni	$⊢ J \in TopOn ({Base}_{G}) \to {Base}_{G} = ⋃ J$
10	8 9	syl	$⊢ G \in TopGrp \to {Base}_{G} = ⋃ J$
11	7 10	eleqtrd	$⊢ G \in TopGrp \to 0_{G} \in ⋃ J$
12		eqid	$⊢ ⋃ J = ⋃ J$
13	12	t1sncld	$⊢ (J \in Fre \land 0_{G} \in ⋃ J) \to \{0_{G}\} \in Clsd (J)$
14	13	expcom	$⊢ 0_{G} \in ⋃ J \to (J \in Fre \to \{0_{G}\} \in Clsd (J))$
15	11 14	syl	$⊢ G \in TopGrp \to (J \in Fre \to \{0_{G}\} \in Clsd (J))$
16	5 1	tgphaus	$⊢ G \in TopGrp \to (J \in Haus \leftrightarrow \{0_{G}\} \in Clsd (J))$
17	15 16	sylibrd	$⊢ G \in TopGrp \to (J \in Fre \to J \in Haus)$
18	2 17	impbid2	$⊢ G \in TopGrp \to (J \in Haus \leftrightarrow J \in Fre)$

Metamath Proof Explorer