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