MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-reg Unicode version

Definition df-reg 17044
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.)
Assertion
Ref Expression
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 ) }
Distinct variable group:    x, j, y, z

Detailed syntax breakdown of Definition df-reg
StepHypRef Expression
1 creg 17037 . 2  class  Reg
2 vy . . . . . . . 8  set  y
3 vz . . . . . . . 8  set  z
42, 3wel 1685 . . . . . . 7  wff  y  e.  z
53cv 1622 . . . . . . . . 9  class  z
6 vj . . . . . . . . . . 11  set  j
76cv 1622 . . . . . . . . . 10  class  j
8 ccl 16755 . . . . . . . . . 10  class  cls
97, 8cfv 5255 . . . . . . . . 9  class  ( cls `  j )
105, 9cfv 5255 . . . . . . . 8  class  ( ( cls `  j ) `
 z )
11 vx . . . . . . . . 9  set  x
1211cv 1622 . . . . . . . 8  class  x
1310, 12wss 3152 . . . . . . 7  wff  ( ( cls `  j ) `
 z )  C_  x
144, 13wa 358 . . . . . 6  wff  ( y  e.  z  /\  (
( cls `  j
) `  z )  C_  x )
1514, 3, 7wrex 2544 . . . . 5  wff  E. z  e.  j  ( y  e.  z  /\  (
( cls `  j
) `  z )  C_  x )
1615, 2, 12wral 2543 . . . 4  wff  A. y  e.  x  E. z  e.  j  ( y  e.  z  /\  (
( cls `  j
) `  z )  C_  x )
1716, 11, 7wral 2543 . . 3  wff  A. x  e.  j  A. y  e.  x  E. z  e.  j  ( y  e.  z  /\  (
( cls `  j
) `  z )  C_  x )
18 ctop 16631 . . 3  class  Top
1917, 6, 18crab 2547 . 2  class  { j  e.  Top  |  A. x  e.  j  A. y  e.  x  E. z  e.  j  (
y  e.  z  /\  ( ( cls `  j
) `  z )  C_  x ) }
201, 19wceq 1623 1  wff  Reg  =  { j  e.  Top  | 
A. x  e.  j 
A. y  e.  x  E. z  e.  j 
( y  e.  z  /\  ( ( cls `  j ) `  z
)  C_  x ) }
Colors of variables: wff set class
This definition is referenced by:  isreg  17060
  Copyright terms: Public domain W3C validator