Metamath Proof Explorer

Theorem ishaus2

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

		Ref	Expression
	Assertion	ishaus2	$⊢ J \in TopOn (X) \to (J \in Haus \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)))$

Proof

Step	Hyp	Ref	Expression
1		topontop	$⊢ J \in TopOn (X) \to J \in Top$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	ishaus	$⊢ J \in Haus \leftrightarrow (J \in Top \land \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)))$
4	3	baib	$⊢ J \in Top \to (J \in Haus \leftrightarrow \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)))$
5	1 4	syl	$⊢ J \in TopOn (X) \to (J \in Haus \leftrightarrow \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)))$
6		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
7	6	raleqdv	$⊢ J \in TopOn (X) \to (\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)) \leftrightarrow \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)))$
8	6 7	raleqbidv	$⊢ J \in TopOn (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)) \leftrightarrow \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)))$
9	5 8	bitr4d	$⊢ J \in TopOn (X) \to (J \in Haus \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)))$