Metamath Proof Explorer

Theorem ist1-5

Description: A topological space is T_1 iff it is both T_0 and R_0. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion ist1-5 
|- ( J e. Fre <-> ( J e. Kol2 /\ ( KQ ` J ) e. Fre ) )

Proof

Step Hyp Ref Expression
1 t1t0 
 |-  ( J e. Fre -> J e. Kol2 )
2 t1hmph 
 |-  ( J ~= ( KQ ` J ) -> ( J e. Fre -> ( KQ ` J ) e. Fre ) )
3 t1hmph 
 |-  ( ( KQ ` J ) ~= J -> ( ( KQ ` J ) e. Fre -> J e. Fre ) )
4 1 2 3 ist1-5lem 
 |-  ( J e. Fre <-> ( J e. Kol2 /\ ( KQ ` J ) e. Fre ) )