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