Metamath Proof Explorer

Theorem kqhmph

Description: A topological space is T_0 iff it is homeomorphic to its Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion kqhmph 
|- ( J e. Kol2 <-> J ~= ( KQ ` J ) )

Proof

Step Hyp Ref Expression
1 t0top 
 |-  ( J e. Kol2 -> J e. Top )
2 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
3 1 2 sylib 
 |-  ( J e. Kol2 -> J e. ( TopOn ` U. J ) )
4 eqid 
 |-  ( x e. U. J |-> { y e. J | x e. y } ) = ( x e. U. J |-> { y e. J | x e. y } )
5 4 t0kq 
 |-  ( J e. ( TopOn ` U. J ) -> ( J e. Kol2 <-> ( x e. U. J |-> { y e. J | x e. y } ) e. ( J Homeo ( KQ ` J ) ) ) )
6 3 5 syl 
 |-  ( J e. Kol2 -> ( J e. Kol2 <-> ( x e. U. J |-> { y e. J | x e. y } ) e. ( J Homeo ( KQ ` J ) ) ) )
7 6 ibi 
 |-  ( J e. Kol2 -> ( x e. U. J |-> { y e. J | x e. y } ) e. ( J Homeo ( KQ ` J ) ) )
8 hmphi 
 |-  ( ( x e. U. J |-> { y e. J | x e. y } ) e. ( J Homeo ( KQ ` J ) ) -> J ~= ( KQ ` J ) )
9 7 8 syl 
 |-  ( J e. Kol2 -> J ~= ( KQ ` J ) )
10 hmphsym 
 |-  ( J ~= ( KQ ` J ) -> ( KQ ` J ) ~= J )
11 hmphtop1 
 |-  ( J ~= ( KQ ` J ) -> J e. Top )
12 kqt0 
 |-  ( J e. Top <-> ( KQ ` J ) e. Kol2 )
13 11 12 sylib 
 |-  ( J ~= ( KQ ` J ) -> ( KQ ` J ) e. Kol2 )
14 t0hmph 
 |-  ( ( KQ ` J ) ~= J -> ( ( KQ ` J ) e. Kol2 -> J e. Kol2 ) )
15 10 13 14 sylc 
 |-  ( J ~= ( KQ ` J ) -> J e. Kol2 )
16 9 15 impbii 
 |-  ( J e. Kol2 <-> J ~= ( KQ ` J ) )