Definition df-haus 17333

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. (Contributed by NM, 8-Mar-2007.)

Assertion

Ref	Expression
df-haus	|- Haus = { j e. Top | A. x e. U. j 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 ) = (/) ) ) }

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

Detailed syntax breakdown of Definition df-haus

Step	Hyp	Ref	Expression
1		cha 17326	. 2 class Haus
2		vx	. . . . . . . 8 set x
3	2	cv 1648	. . . . . . 7 class x
4		vy	. . . . . . . 8 set y
5	4	cv 1648	. . . . . . 7 class y
6	3, 5	wne 2567	. . . . . 6 wff x =/= y
7		vn	. . . . . . . . . 10 set n
8	2, 7	wel 1722	. . . . . . . . 9 wff x e. n
9		vm	. . . . . . . . . 10 set m
10	4, 9	wel 1722	. . . . . . . . 9 wff y e. m
11	7	cv 1648	. . . . . . . . . . 11 class n
12	9	cv 1648	. . . . . . . . . . 11 class m
13	11, 12	cin 3279	. . . . . . . . . 10 class ( n i^i m )
14		c0 3588	. . . . . . . . . 10 class (/)
15	13, 14	wceq 1649	. . . . . . . . 9 wff ( n i^i m ) = (/)
16	8, 10, 15	w3a 936	. . . . . . . 8 wff ( x e. n /\ y e. m /\ ( n i^i m ) = (/) )
17		vj	. . . . . . . . 9 set j
18	17	cv 1648	. . . . . . . 8 class j
19	16, 9, 18	wrex 2667	. . . . . . 7 wff E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) )
20	19, 7, 18	wrex 2667	. . . . . 6 wff E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) )
21	6, 20	wi 4	. . . . 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 3975	. . . . 5 class U. j
23	21, 4, 22	wral 2666	. . . 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 2666	. . 3 wff A. x e. U. j 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 ) = (/) ) )
25		ctop 16913	. . 3 class Top
26	24, 17, 25	crab 2670	. 2 class { j e. Top | A. x e. U. j 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 ) = (/) ) ) }
27	1, 26	wceq 1649	1 wff Haus = { j e. Top | A. x e. U. j 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 ) = (/) ) ) }

This definition is referenced by:  ishaus  17340