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 = ⋃ J$
	Assertion	t1sep	$⊢ (J \in Fre \land (A \in X \land B \in X \land A \neq B)) \to \exists o \in J (A \in o \land \neg B \in o)$

Step	Hyp	Ref	Expression
1		t1sep.1	$⊢ X = ⋃ J$
2		simpr3	$⊢ (J \in Fre \land (A \in X \land B \in X \land A \neq B)) \to A \neq B$
3	1	t1sep2	$⊢ (J \in Fre \land A \in X \land B \in X) \to (\forall o \in J (A \in o \to B \in o) \to A = B)$
4	3	3adant3r3	$⊢ (J \in Fre \land (A \in X \land B \in X \land A \neq B)) \to (\forall o \in J (A \in o \to B \in o) \to A = B)$
5	4	necon3ad	$⊢ (J \in Fre \land (A \in X \land B \in X \land A \neq B)) \to (A \neq B \to \neg \forall o \in J (A \in o \to B \in o))$
6	2 5	mpd	$⊢ (J \in Fre \land (A \in X \land B \in X \land A \neq B)) \to \neg \forall o \in J (A \in o \to B \in o)$
7		rexanali	$⊢ \exists o \in J (A \in o \land \neg B \in o) \leftrightarrow \neg \forall o \in J (A \in o \to B \in o)$
8	6 7	sylibr	$⊢ (J \in Fre \land (A \in X \land B \in X \land A \neq B)) \to \exists o \in J (A \in o \land \neg B \in o)$

Metamath Proof Explorer