Metamath Proof Explorer

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 = { 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 ) = (/) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cha 
 |-  Haus
1 vj 
 |-  j
2 ctop 
 |-  Top
3 vx 
 |-  x
4 1 cv 
 |-  j
5 4 cuni 
 |-  U. j
6 vy 
 |-  y
7 3 cv 
 |-  x
8 6 cv 
 |-  y
9 7 8 wne 
 |-  x =/= y
10 vn 
 |-  n
11 vm 
 |-  m
12 10 cv 
 |-  n
13 7 12 wcel 
 |-  x e. n
14 11 cv 
 |-  m
15 8 14 wcel 
 |-  y e. m
16 12 14 cin 
 |-  ( n i^i m )
17 c0 
 |-  (/)
18 16 17 wceq 
 |-  ( n i^i m ) = (/)
19 13 15 18 w3a 
 |-  ( x e. n /\ y e. m /\ ( n i^i m ) = (/) )
20 19 11 4 wrex 
 |-  E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) )
21 20 10 4 wrex 
 |-  E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) )
22 9 21 wi 
 |-  ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) )
23 22 6 5 wral 
 |-  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 3 5 wral 
 |-  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 24 1 2 crab 
 |-  { 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 ) = (/) ) ) }
26 0 25 wceq 
 |-  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 ) = (/) ) ) }