Definition df-haus 21119

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 21112	. 2 class Haus
2		vx	. . . . . . . 8 setvar x
3	2	cv 1482	. . . . . . 7 class x
4		vy	. . . . . . . 8 setvar y
5	4	cv 1482	. . . . . . 7 class y
6	3, 5	wne 2794	. . . . . 6 wff x =/= y
7		vn	. . . . . . . . . 10 setvar n
8	2, 7	wel 1991	. . . . . . . . 9 wff x e. n
9		vm	. . . . . . . . . 10 setvar m
10	4, 9	wel 1991	. . . . . . . . 9 wff y e. m
11	7	cv 1482	. . . . . . . . . . 11 class n
12	9	cv 1482	. . . . . . . . . . 11 class m
13	11, 12	cin 3573	. . . . . . . . . 10 class ( n i^i m )
14		c0 3915	. . . . . . . . . 10 class (/)
15	13, 14	wceq 1483	. . . . . . . . 9 wff ( n i^i m ) = (/)
16	8, 10, 15	w3a 1037	. . . . . . . 8 wff ( x e. n /\ y e. m /\ ( n i^i m ) = (/) )
17		vj	. . . . . . . . 9 setvar j
18	17	cv 1482	. . . . . . . 8 class j
19	16, 9, 18	wrex 2913	. . . . . . 7 wff E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) )
20	19, 7, 18	wrex 2913	. . . . . 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 4436	. . . . 5 class U. j
23	21, 4, 22	wral 2912	. . . 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 2912	. . 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 20698	. . 3 class Top
26	24, 17, 25	crab 2916	. 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 1483	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  21126