This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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