Metamath Proof Explorer

Theorem hausnei

Description: Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007)

		Ref	Expression
	Hypothesis	ist0.1	$⊢ X = ⋃ J$
	Assertion	hausnei	$⊢ (J \in Haus \land (P \in X \land Q \in X \land P \neq Q)) \to \exists n \in J \exists m \in J (P \in n \land Q \in m \land n \cap m = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		ist0.1	$⊢ X = ⋃ J$
2	1	ishaus	$⊢ J \in Haus \leftrightarrow (J \in Top \land \forall x \in X \forall y \in X (x \neq y \to \exists n \in J \exists m \in J (x \in n \land y \in m \land n \cap m = \emptyset)))$
3	2	simprbi	$⊢ J \in Haus \to \forall x \in X \forall y \in X (x \neq y \to \exists n \in J \exists m \in J (x \in n \land y \in m \land n \cap m = \emptyset))$
4		neeq1	$⊢ x = P \to (x \neq y \leftrightarrow P \neq y)$
5		eleq1	$⊢ x = P \to (x \in n \leftrightarrow P \in n)$
6	5	3anbi1d	$⊢ x = P \to ((x \in n \land y \in m \land n \cap m = \emptyset) \leftrightarrow (P \in n \land y \in m \land n \cap m = \emptyset))$
7	6	2rexbidv	$⊢ x = P \to (\exists n \in J \exists m \in J (x \in n \land y \in m \land n \cap m = \emptyset) \leftrightarrow \exists n \in J \exists m \in J (P \in n \land y \in m \land n \cap m = \emptyset))$
8	4 7	imbi12d	$⊢ x = P \to ((x \neq y \to \exists n \in J \exists m \in J (x \in n \land y \in m \land n \cap m = \emptyset)) \leftrightarrow (P \neq y \to \exists n \in J \exists m \in J (P \in n \land y \in m \land n \cap m = \emptyset)))$
9		neeq2	$⊢ y = Q \to (P \neq y \leftrightarrow P \neq Q)$
10		eleq1	$⊢ y = Q \to (y \in m \leftrightarrow Q \in m)$
11	10	3anbi2d	$⊢ y = Q \to ((P \in n \land y \in m \land n \cap m = \emptyset) \leftrightarrow (P \in n \land Q \in m \land n \cap m = \emptyset))$
12	11	2rexbidv	$⊢ y = Q \to (\exists n \in J \exists m \in J (P \in n \land y \in m \land n \cap m = \emptyset) \leftrightarrow \exists n \in J \exists m \in J (P \in n \land Q \in m \land n \cap m = \emptyset))$
13	9 12	imbi12d	$⊢ y = Q \to ((P \neq y \to \exists n \in J \exists m \in J (P \in n \land y \in m \land n \cap m = \emptyset)) \leftrightarrow (P \neq Q \to \exists n \in J \exists m \in J (P \in n \land Q \in m \land n \cap m = \emptyset)))$
14	8 13	rspc2v	$⊢ (P \in X \land Q \in X) \to (\forall x \in X \forall y \in X (x \neq y \to \exists n \in J \exists m \in J (x \in n \land y \in m \land n \cap m = \emptyset)) \to (P \neq Q \to \exists n \in J \exists m \in J (P \in n \land Q \in m \land n \cap m = \emptyset)))$
15	3 14	syl5	$⊢ (P \in X \land Q \in X) \to (J \in Haus \to (P \neq Q \to \exists n \in J \exists m \in J (P \in n \land Q \in m \land n \cap m = \emptyset)))$
16	15	ex	$⊢ P \in X \to (Q \in X \to (J \in Haus \to (P \neq Q \to \exists n \in J \exists m \in J (P \in n \land Q \in m \land n \cap m = \emptyset))))$
17	16	com3r	$⊢ J \in Haus \to (P \in X \to (Q \in X \to (P \neq Q \to \exists n \in J \exists m \in J (P \in n \land Q \in m \land n \cap m = \emptyset))))$
18	17	3imp2	$⊢ (J \in Haus \land (P \in X \land Q \in X \land P \neq Q)) \to \exists n \in J \exists m \in J (P \in n \land Q \in m \land n \cap m = \emptyset)$