# 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 ) )`
` |-  ( ( 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 ) ) ) )`