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=⋃J
Assertion t0dist ⊢J∈Kol2∧A∈X∧B∈X∧A≠B→∃o∈J¬A∈o↔B∈o

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢X=⋃J
2 1 t0sep ⊢J∈Kol2∧A∈X∧B∈X→∀o∈JA∈o↔B∈o→A=B
3 2 necon3ad ⊢J∈Kol2∧A∈X∧B∈X→A≠B→¬∀o∈JA∈o↔B∈o
4 3 exp32 ⊢J∈Kol2→A∈X→B∈X→A≠B→¬∀o∈JA∈o↔B∈o
5 4 3imp2 ⊢J∈Kol2∧A∈X∧B∈X∧A≠B→¬∀o∈JA∈o↔B∈o
6 rexnal ⊢∃o∈J¬A∈o↔B∈o↔¬∀o∈JA∈o↔B∈o
7 5 6 sylibr ⊢J∈Kol2∧A∈X∧B∈X∧A≠B→∃o∈J¬A∈o↔B∈o