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