# Metamath Proof Explorer

## Theorem t0dist

Description: Any two distinct points in a T_0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Hypothesis ist0.1 ${⊢}{X}=\bigcup {J}$
Assertion t0dist ${⊢}\left({J}\in \mathrm{Kol2}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {A}\ne {B}\right)\right)\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}¬\left({A}\in {o}↔{B}\in {o}\right)$

### Proof

Step Hyp Ref Expression
1 ist0.1 ${⊢}{X}=\bigcup {J}$
2 1 t0sep ${⊢}\left({J}\in \mathrm{Kol2}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to \left(\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {o}↔{B}\in {o}\right)\to {A}={B}\right)$
3 2 necon3ad ${⊢}\left({J}\in \mathrm{Kol2}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to \left({A}\ne {B}\to ¬\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {o}↔{B}\in {o}\right)\right)$
4 3 exp32 ${⊢}{J}\in \mathrm{Kol2}\to \left({A}\in {X}\to \left({B}\in {X}\to \left({A}\ne {B}\to ¬\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {o}↔{B}\in {o}\right)\right)\right)\right)$
5 4 3imp2 ${⊢}\left({J}\in \mathrm{Kol2}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {A}\ne {B}\right)\right)\to ¬\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {o}↔{B}\in {o}\right)$
6 rexnal ${⊢}\exists {o}\in {J}\phantom{\rule{.4em}{0ex}}¬\left({A}\in {o}↔{B}\in {o}\right)↔¬\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {o}↔{B}\in {o}\right)$
7 5 6 sylibr ${⊢}\left({J}\in \mathrm{Kol2}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {A}\ne {B}\right)\right)\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}¬\left({A}\in {o}↔{B}\in {o}\right)$