Theorem t0kq

Description: A topological space is T_0 iff the quotient map is a homeomorphism onto the space's Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	t0kq.1	|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion	t0kq	|- ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> F e. ( J Homeo ( KQ ` J ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		t0kq.1	|- F = ( x e. X |-> { y e. J | x e. y } )
2		simpl	|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> J e. ( TopOn ` X ) )
3	1	ist0-4	|- ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> F : X -1-1-> _V ) )
4	3	biimpa	|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> F : X -1-1-> _V )
5	2 4	qtopf1	|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> F e. ( J Homeo ( J qTop F ) ) )
6	1	kqval	|- ( J e. ( TopOn ` X ) -> ( KQ ` J ) = ( J qTop F ) )
7	6	adantr	|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> ( KQ ` J ) = ( J qTop F ) )
8	7	oveq2d	|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> ( J Homeo ( KQ ` J ) ) = ( J Homeo ( J qTop F ) ) )
9	5 8	eleqtrrd	|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> F e. ( J Homeo ( KQ ` J ) ) )
10		hmphi	|- ( F e. ( J Homeo ( KQ ` J ) ) -> J ~= ( KQ ` J ) )
11		hmphsym	|- ( J ~= ( KQ ` J ) -> ( KQ ` J ) ~= J )
12	10 11	syl	|- ( F e. ( J Homeo ( KQ ` J ) ) -> ( KQ ` J ) ~= J )
13	1	kqt0lem	|- ( J e. ( TopOn ` X ) -> ( KQ ` J ) e. Kol2 )
14		t0hmph	|- ( ( KQ ` J ) ~= J -> ( ( KQ ` J ) e. Kol2 -> J e. Kol2 ) )
15	12 13 14	syl2im	|- ( F e. ( J Homeo ( KQ ` J ) ) -> ( J e. ( TopOn ` X ) -> J e. Kol2 ) )
16	15	impcom	|- ( ( J e. ( TopOn ` X ) /\ F e. ( J Homeo ( KQ ` J ) ) ) -> J e. Kol2 )
17	9 16	impbida	|- ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> F e. ( J Homeo ( KQ ` J ) ) ) )