Definition df-haus 9059

Description: Define the class of all Hausdorff spaces. A Hausdorff space is a topology in which distinct points have disjoint open neighborhoods. Definition of Hausdorff space in [Munkres] p. 98.

Assertion

Ref	Expression
df-haus	|- Haus = {j e. Top | A.x e. U.jA.y e. U.j(x =/= y -> E.n e. j E.m e. j (x e. n /\ y e. m /\ (n i^i m) = (/)))}

Distinct variable group:   j,m,n,x,y

Detailed syntax breakdown of Definition df-haus

Step	Hyp	Ref	Expression
1		cha 9058	. 2 class Haus
2		vx	. . . . . . . 8 set x
3	2	cv 1297	. . . . . . 7 class x
4		vy	. . . . . . . 8 set y
5	4	cv 1297	. . . . . . 7 class y
6	3, 5	wne 2017	. . . . . 6 wff x =/= y
7		vn	. . . . . . . . . . 11 set n
8	7	cv 1297	. . . . . . . . . 10 class n
9	3, 8	wcel 1300	. . . . . . . . 9 wff x e. n
10		vm	. . . . . . . . . . 11 set m
11	10	cv 1297	. . . . . . . . . 10 class m
12	5, 11	wcel 1300	. . . . . . . . 9 wff y e. m
13	8, 11	cin 2592	. . . . . . . . . 10 class (n i^i m)
14		c0 2875	. . . . . . . . . 10 class (/)
15	13, 14	wceq 1298	. . . . . . . . 9 wff (n i^i m) = (/)
16	9, 12, 15	w3a 858	. . . . . . . 8 wff (x e. n /\ y e. m /\ (n i^i m) = (/))
17		vj	. . . . . . . . 9 set j
18	17	cv 1297	. . . . . . . 8 class j
19	16, 10, 18	wrex 2106	. . . . . . 7 wff E.m e. j (x e. n /\ y e. m /\ (n i^i m) = (/))
20	19, 7, 18	wrex 2106	. . . . . 6 wff E.n e. j E.m e. j (x e. n /\ y e. m /\ (n i^i m) = (/))
21	6, 20	wi 3	. . . . 5 wff (x =/= y -> E.n e. j E.m e. j (x e. n /\ y e. m /\ (n i^i m) = (/)))
22	18	cuni 3177	. . . . 5 class U.j
23	21, 4, 22	wral 2105	. . . 4 wff A.y e. U.j(x =/= y -> E.n e. j E.m e. j (x e. n /\ y e. m /\ (n i^i m) = (/)))
24	23, 2, 22	wral 2105	. . 3 wff A.x e. U.jA.y e. U.j(x =/= y -> E.n e. j E.m e. j (x e. n /\ y e. m /\ (n i^i m) = (/)))
25		ctop 8857	. . 3 class Top
26	24, 17, 25	crab 2108	. 2 class {j e. Top | A.x e. U.jA.y e. U.j(x =/= y -> E.n e. j E.m e. j (x e. n /\ y e. m /\ (n i^i m) = (/)))}
27	1, 26	wceq 1298	1 wff Haus = {j e. Top | A.x e. U.jA.y e. U.j(x =/= y -> E.n e. j E.m e. j (x e. n /\ y e. m /\ (n i^i m) = (/)))}

This definition is referenced by:  ishaus 9060

Copyright terms: Public domain