Theorem kqt0

Description: The Kolmogorov quotient is T_0 even if the original topology is not. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Assertion	kqt0	|- ( J e. Top <-> ( KQ ` J ) e. Kol2 )

Proof

Step	Hyp	Ref	Expression
1		toptopon2	|- ( J e. Top <-> J e. ( TopOn ` U. J ) )
2		eqid	|- ( x e. U. J |-> { y e. J | x e. y } ) = ( x e. U. J |-> { y e. J | x e. y } )
3	2	kqt0lem	|- ( J e. ( TopOn ` U. J ) -> ( KQ ` J ) e. Kol2 )
4	1 3	sylbi	|- ( J e. Top -> ( KQ ` J ) e. Kol2 )
5		t0top	|- ( ( KQ ` J ) e. Kol2 -> ( KQ ` J ) e. Top )
6		kqtop	|- ( J e. Top <-> ( KQ ` J ) e. Top )
7	5 6	sylibr	|- ( ( KQ ` J ) e. Kol2 -> J e. Top )
8	4 7	impbii	|- ( J e. Top <-> ( KQ ` J ) e. Kol2 )