df-haus

Description: Define the class of all Hausdorff (or T_2) spaces. A Hausdorff space is a topology in which distinct points have disjoint open neighborhoods. Definition of Hausdorff space in Munkres p. 98. (Contributed by NM, 8-Mar-2007)

		Ref	Expression
	Assertion	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))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cha	$class Haus$
1		vj	$setvar j$
2		ctop	$class Top$
3		vx	$setvar x$
4	1	cv	$setvar j$
5	4	cuni	$class ⋃ j$
6		vy	$setvar y$
7	3	cv	$setvar x$
8	6	cv	$setvar y$
9	7 8	wne	$wff x \neq y$
10		vn	$setvar n$
11		vm	$setvar m$
12	10	cv	$setvar n$
13	7 12	wcel	$wff x \in n$
14	11	cv	$setvar m$
15	8 14	wcel	$wff y \in m$
16	12 14	cin	$class (n \cap m)$
17		c0	$class \emptyset$
18	16 17	wceq	$wff n \cap m = \emptyset$
19	13 15 18	w3a	$wff (x \in n \land y \in m \land n \cap m = \emptyset)$
20	19 11 4	wrex	$wff \exists m \in j (x \in n \land y \in m \land n \cap m = \emptyset)$
21	20 10 4	wrex	$wff \exists n \in j \exists m \in j (x \in n \land y \in m \land n \cap m = \emptyset)$
22	9 21	wi	$wff (x \neq y \to \exists n \in j \exists m \in j (x \in n \land y \in m \land n \cap m = \emptyset))$
23	22 6 5	wral	$wff \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))$
24	23 3 5	wral	$wff \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))$
25	24 1 2	crab	$class \{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))\}$
26	0 25	wceq	$wff 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))\}$

Metamath Proof Explorer

Definition df-haus

Detailed syntax breakdown