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

Definition df-cld 16751
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 16748 . 2  class  Clsd
2 vj . . 3  set  j
3 ctop 16626 . . 3  class  Top
42cv 1623 . . . . . . 7  class  j
54cuni 3829 . . . . . 6  class  U. j
6 vx . . . . . . 7  set  x
76cv 1623 . . . . . 6  class  x
85, 7cdif 3151 . . . . 5  class  ( U. j  \  x )
98, 4wcel 1685 . . . 4  wff  ( U. j  \  x )  e.  j
105cpw 3627 . . . 4  class  ~P U. j
119, 6, 10crab 2549 . . 3  class  { x  e.  ~P U. j  |  ( U. j  \  x )  e.  j }
122, 3, 11cmpt 4079 . 2  class  ( j  e.  Top  |->  { x  e.  ~P U. j  |  ( U. j  \  x )  e.  j } )
131, 12wceq 1624 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  16754  cldval  16755
  Copyright terms: Public domain W3C validator