This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-reg

Description: Define regular spaces. A space is regular if a point and a closed set can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion df-reg 
|- Reg = { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 creg 
 |-  Reg
1 vj 
 |-  j
2 ctop 
 |-  Top
3 vx 
 |-  x
4 1 cv 
 |-  j
5 vy 
 |-  y
6 3 cv 
 |-  x
7 vz 
 |-  z
8 5 cv 
 |-  y
9 7 cv 
 |-  z
10 8 9 wcel 
 |-  y e. z
11 ccl 
 |-  cls
12 4 11 cfv 
 |-  ( cls ` j )
13 9 12 cfv 
 |-  ( ( cls ` j ) ` z )
14 13 6 wss 
 |-  ( ( cls ` j ) ` z ) C_ x
15 10 14 wa 
 |-  ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
16 15 7 4 wrex 
 |-  E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
17 16 5 6 wral 
 |-  A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
18 17 3 4 wral 
 |-  A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
19 18 1 2 crab 
 |-  { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }
20 0 19 wceq 
 |-  Reg = { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }