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

Definition df-nrm 17045
Description: Define normal spaces. A space is normal if disjoint closed sets can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.)
Assertion
Ref Expression
df-nrm  |-  Nrm  =  { j  e.  Top  | 
A. x  e.  j 
A. y  e.  ( ( Clsd `  j
)  i^i  ~P x
) E. z  e.  j  ( y  C_  z  /\  ( ( cls `  j ) `  z
)  C_  x ) }
Distinct variable group:    x, j, y, z

Detailed syntax breakdown of Definition df-nrm
StepHypRef Expression
1 cnrm 17038 . 2  class  Nrm
2 vy . . . . . . . . 9  set  y
32cv 1622 . . . . . . . 8  class  y
4 vz . . . . . . . . 9  set  z
54cv 1622 . . . . . . . 8  class  z
63, 5wss 3152 . . . . . . 7  wff  y  C_  z
7 vj . . . . . . . . . . 11  set  j
87cv 1622 . . . . . . . . . 10  class  j
9 ccl 16755 . . . . . . . . . 10  class  cls
108, 9cfv 5255 . . . . . . . . 9  class  ( cls `  j )
115, 10cfv 5255 . . . . . . . 8  class  ( ( cls `  j ) `
 z )
12 vx . . . . . . . . 9  set  x
1312cv 1622 . . . . . . . 8  class  x
1411, 13wss 3152 . . . . . . 7  wff  ( ( cls `  j ) `
 z )  C_  x
156, 14wa 358 . . . . . 6  wff  ( y 
C_  z  /\  (
( cls `  j
) `  z )  C_  x )
1615, 4, 8wrex 2544 . . . . 5  wff  E. z  e.  j  ( y  C_  z  /\  ( ( cls `  j ) `
 z )  C_  x )
17 ccld 16753 . . . . . . 7  class  Clsd
188, 17cfv 5255 . . . . . 6  class  ( Clsd `  j )
1913cpw 3625 . . . . . 6  class  ~P x
2018, 19cin 3151 . . . . 5  class  ( (
Clsd `  j )  i^i  ~P x )
2116, 2, 20wral 2543 . . . 4  wff  A. y  e.  ( ( Clsd `  j
)  i^i  ~P x
) E. z  e.  j  ( y  C_  z  /\  ( ( cls `  j ) `  z
)  C_  x )
2221, 12, 8wral 2543 . . 3  wff  A. x  e.  j  A. y  e.  ( ( Clsd `  j
)  i^i  ~P x
) E. z  e.  j  ( y  C_  z  /\  ( ( cls `  j ) `  z
)  C_  x )
23 ctop 16631 . . 3  class  Top
2422, 7, 23crab 2547 . 2  class  { j  e.  Top  |  A. x  e.  j  A. y  e.  ( ( Clsd `  j )  i^i 
~P x ) E. z  e.  j  ( y  C_  z  /\  ( ( cls `  j
) `  z )  C_  x ) }
251, 24wceq 1623 1  wff  Nrm  =  { j  e.  Top  | 
A. x  e.  j 
A. y  e.  ( ( Clsd `  j
)  i^i  ~P x
) E. z  e.  j  ( y  C_  z  /\  ( ( cls `  j ) `  z
)  C_  x ) }
Colors of variables: wff set class
This definition is referenced by:  isnrm  17063
  Copyright terms: Public domain W3C validator