Theorem t1sep

Description: Any two distinct points in a T_1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010)

	Ref	Expression
Hypothesis	t1sep.1	|- X = U. J
Assertion	t1sep	|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> E. o e. J ( A e. o /\ -. B e. o ) )

Proof

Step	Hyp	Ref	Expression
1		t1sep.1	|- X = U. J
2		simpr3	|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> A =/= B )
3	1	t1sep2	|- ( ( J e. Fre /\ A e. X /\ B e. X ) -> ( A. o e. J ( A e. o -> B e. o ) -> A = B ) )
4	3	3adant3r3	|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> ( A. o e. J ( A e. o -> B e. o ) -> A = B ) )
5	4	necon3ad	|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> ( A =/= B -> -. A. o e. J ( A e. o -> B e. o ) ) )
6	2 5	mpd	|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> -. A. o e. J ( A e. o -> B e. o ) )
7		rexanali	|- ( E. o e. J ( A e. o /\ -. B e. o ) <-> -. A. o e. J ( A e. o -> B e. o ) )
8	6 7	sylibr	|- ( ( J e. Fre /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> E. o e. J ( A e. o /\ -. B e. o ) )