Theorem ishaus3

Description: A topological space is Hausdorff iff it is both T_0 and R_1 (where R_1 means that any two topologically distinct points are separated by neighborhoods). (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Assertion	ishaus3	|- ( J e. Haus <-> ( J e. Kol2 /\ ( KQ ` J ) e. Haus ) )

Proof

Step	Hyp	Ref	Expression
1		haust1	|- ( J e. Haus -> J e. Fre )
2		t1t0	|- ( J e. Fre -> J e. Kol2 )
3	1 2	syl	|- ( J e. Haus -> J e. Kol2 )
4		haushmph	|- ( J ~= ( KQ ` J ) -> ( J e. Haus -> ( KQ ` J ) e. Haus ) )
5		haushmph	|- ( ( KQ ` J ) ~= J -> ( ( KQ ` J ) e. Haus -> J e. Haus ) )
6	3 4 5	ist1-5lem	|- ( J e. Haus <-> ( J e. Kol2 /\ ( KQ ` J ) e. Haus ) )