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

Definition df-cld 16756
Description: Define a function on topologies whose value is the set of closed sets of the topology. (Contributed by NM, 2-Oct-2006.)
Assertion
Ref Expression
df-cld  |-  Clsd  =  ( j  e.  Top  |->  { x  e.  ~P U. j  |  ( U. j  \  x )  e.  j } )
Distinct variable group:    x, j

Detailed syntax breakdown of Definition df-cld
StepHypRef Expression
1 ccld 16753 . 2  class  Clsd
2 vj . . 3  set  j
3 ctop 16631 . . 3  class  Top
42cv 1622 . . . . . . 7  class  j
54cuni 3827 . . . . . 6  class  U. j
6 vx . . . . . . 7  set  x
76cv 1622 . . . . . 6  class  x
85, 7cdif 3149 . . . . 5  class  ( U. j  \  x )
98, 4wcel 1684 . . . 4  wff  ( U. j  \  x )  e.  j
105cpw 3625 . . . 4  class  ~P U. j
119, 6, 10crab 2547 . . 3  class  { x  e.  ~P U. j  |  ( U. j  \  x )  e.  j }
122, 3, 11cmpt 4077 . 2  class  ( j  e.  Top  |->  { x  e.  ~P U. j  |  ( U. j  \  x )  e.  j } )
131, 12wceq 1623 1  wff  Clsd  =  ( j  e.  Top  |->  { x  e.  ~P U. j  |  ( U. j  \  x )  e.  j } )
Colors of variables: wff set class
This definition is referenced by:  fncld  16759  cldval  16760
  Copyright terms: Public domain W3C validator