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

Metamath Proof Explorer

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