Metamath Proof Explorer


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