Definition df-haus 23323

Description: Define the class of all Hausdorff (or T₂) 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.)

Assertion

Ref	Expression
df-haus	⊢ Haus = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))}

Distinct variable group:   𝑗,𝑚,𝑛,𝑥,𝑦

Detailed syntax breakdown of Definition df-haus

Step	Hyp	Ref	Expression
1		cha 23316	. 2 class Haus
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1539	. . . . . . 7 class 𝑥
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1539	. . . . . . 7 class 𝑦
6	3, 5	wne 2940	. . . . . 6 wff 𝑥 ≠ 𝑦
7		vn	. . . . . . . . . 10 setvar 𝑛
8	2, 7	wel 2109	. . . . . . . . 9 wff 𝑥 ∈ 𝑛
9		vm	. . . . . . . . . 10 setvar 𝑚
10	4, 9	wel 2109	. . . . . . . . 9 wff 𝑦 ∈ 𝑚
11	7	cv 1539	. . . . . . . . . . 11 class 𝑛
12	9	cv 1539	. . . . . . . . . . 11 class 𝑚
13	11, 12	cin 3950	. . . . . . . . . 10 class (𝑛 ∩ 𝑚)
14		c0 4333	. . . . . . . . . 10 class ∅
15	13, 14	wceq 1540	. . . . . . . . 9 wff (𝑛 ∩ 𝑚) = ∅
16	8, 10, 15	w3a 1087	. . . . . . . 8 wff (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)
17		vj	. . . . . . . . 9 setvar 𝑗
18	17	cv 1539	. . . . . . . 8 class 𝑗
19	16, 9, 18	wrex 3070	. . . . . . 7 wff ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)
20	19, 7, 18	wrex 3070	. . . . . 6 wff ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)
21	6, 20	wi 4	. . . . 5 wff (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
22	18	cuni 4907	. . . . 5 class ∪ 𝑗
23	21, 4, 22	wral 3061	. . . 4 wff ∀𝑦 ∈ ∪ 𝑗(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
24	23, 2, 22	wral 3061	. . 3 wff ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
25		ctop 22899	. . 3 class Top
26	24, 17, 25	crab 3436	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))}
27	1, 26	wceq 1540	1 wff Haus = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))}

This definition is referenced by:  ishaus  23330