Metamath Proof Explorer

Theorem fncld

Description: The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion fncld 
|- Clsd Fn Top

Proof

Step Hyp Ref Expression
1 vuniex 
 |-  U. j e. _V
2 1 pwex 
 |-  ~P U. j e. _V
3 2 rabex 
 |-  { x e. ~P U. j | ( U. j \ x ) e. j } e. _V
4 df-cld 
 |-  Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
5 3 4 fnmpti 
 |-  Clsd Fn Top