Definition 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 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cha	⊢ Haus
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑗
5	4	cuni	⊢ ∪ 𝑗
6		vy	⊢ 𝑦
7	3	cv	⊢ 𝑥
8	6	cv	⊢ 𝑦
9	7 8	wne	⊢ 𝑥 ≠ 𝑦
10		vn	⊢ 𝑛
11		vm	⊢ 𝑚
12	10	cv	⊢ 𝑛
13	7 12	wcel	⊢ 𝑥 ∈ 𝑛
14	11	cv	⊢ 𝑚
15	8 14	wcel	⊢ 𝑦 ∈ 𝑚
16	12 14	cin	⊢ ( 𝑛 ∩ 𝑚 )
17		c0	⊢ ∅
18	16 17	wceq	⊢ ( 𝑛 ∩ 𝑚 ) = ∅
19	13 15 18	w3a	⊢ ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ )
20	19 11 4	wrex	⊢ ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ )
21	20 10 4	wrex	⊢ ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ )
22	9 21	wi	⊢ ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
23	22 6 5	wral	⊢ ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
24	23 3 5	wral	⊢ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
25	24 1 2	crab	⊢ { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) }
26	0 25	wceq	⊢ Haus = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) }