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

Metamath Proof Explorer

Theorem ishaus

Description: The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007)

		Ref	Expression
	Hypothesis	ist0.1	$⊢ X = ⋃ J$
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		ist0.1	$⊢ X = ⋃ J$
2		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
3	2 1	eqtr4di	$⊢ j = J \to ⋃ j = X$
4		rexeq	$⊢ j = J \to (\exists m \in j (x \in n \land y \in m \land n \cap m = \emptyset) \leftrightarrow \exists m \in J (x \in n \land y \in m \land n \cap m = \emptyset))$
5	4	rexeqbi1dv	$⊢ j = J \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 (x \in n \land y \in m \land n \cap m = \emptyset))$
6	5	imbi2d	$⊢ j = J \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 (x \neq y \to \exists n \in J \exists m \in J (x \in n \land y \in m \land n \cap m = \emptyset)))$
7	3 6	raleqbidv	$⊢ j = J \to (\forall y \in ⋃ j (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 \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)))$
8	3 7	raleqbidv	$⊢ j = J \to (\forall x \in ⋃ j \forall y \in ⋃ j (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 \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)))$
9		df-haus	$⊢ Haus = \{j \in Top \| \forall x \in ⋃ j \forall y \in ⋃ j (x \neq y \to \exists n \in j \exists m \in j (x \in n \land y \in m \land n \cap m = \emptyset))\}$
10	8 9	elrab2	$⊢ 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)))$