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