This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = U. J
Assertion t0dist 
|- ( ( J e. Kol2 /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> E. o e. J -. ( A e. o <-> B e. o ) )

Proof

Step Hyp Ref Expression
1 ist0.1 
 |-  X = U. J
2 1 t0sep 
 |-  ( ( J e. Kol2 /\ ( A e. X /\ B e. X ) ) -> ( A. o e. J ( A e. o <-> B e. o ) -> A = B ) )
3 2 necon3ad 
 |-  ( ( J e. Kol2 /\ ( A e. X /\ B e. X ) ) -> ( A =/= B -> -. A. o e. J ( A e. o <-> B e. o ) ) )
4 3 exp32 
 |-  ( J e. Kol2 -> ( A e. X -> ( B e. X -> ( A =/= B -> -. A. o e. J ( A e. o <-> B e. o ) ) ) ) )
5 4 3imp2 
 |-  ( ( J e. Kol2 /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> -. A. o e. J ( A e. o <-> B e. o ) )
6 rexnal 
 |-  ( E. o e. J -. ( A e. o <-> B e. o ) <-> -. A. o e. J ( A e. o <-> B e. o ) )
7 5 6 sylibr 
 |-  ( ( J e. Kol2 /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> E. o e. J -. ( A e. o <-> B e. o ) )