ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-cld Unicode version

Definition df-cld 12301
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 12298 . 2  class  Clsd
2 vj . . 3  setvar  j
3 ctop 12201 . . 3  class  Top
42cv 1331 . . . . . . 7  class  j
54cuni 3743 . . . . . 6  class  U. j
6 vx . . . . . . 7  setvar  x
76cv 1331 . . . . . 6  class  x
85, 7cdif 3072 . . . . 5  class  ( U. j  \  x )
98, 4wcel 1481 . . . 4  wff  ( U. j  \  x )  e.  j
105cpw 3514 . . . 4  class  ~P U. j
119, 6, 10crab 2421 . . 3  class  { x  e.  ~P U. j  |  ( U. j  \  x )  e.  j }
122, 3, 11cmpt 3996 . 2  class  ( j  e.  Top  |->  { x  e.  ~P U. j  |  ( U. j  \  x )  e.  j } )
131, 12wceq 1332 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  12304  cldval  12305
  Copyright terms: Public domain W3C validator