Theorem clsf

Description: The closure function is a function from subsets of the base to closed sets. (Contributed by Mario Carneiro, 11-Apr-2015)

	Ref	Expression
Hypothesis	clscld.1	|- X = U. J
Assertion	clsf	|- ( J e. Top -> ( cls ` J ) : ~P X --> ( Clsd ` J ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2		elpwi	|- ( x e. ~P X -> x C_ X )
3	1	clsval	|- ( ( J e. Top /\ x C_ X ) -> ( ( cls ` J ) ` x ) = |^| { y e. ( Clsd ` J ) | x C_ y } )
4		fvex	|- ( ( cls ` J ) ` x ) e. _V
5	3 4	eqeltrrdi	|- ( ( J e. Top /\ x C_ X ) -> |^| { y e. ( Clsd ` J ) | x C_ y } e. _V )
6	2 5	sylan2	|- ( ( J e. Top /\ x e. ~P X ) -> |^| { y e. ( Clsd ` J ) | x C_ y } e. _V )
7	1	clsfval	|- ( J e. Top -> ( cls ` J ) = ( x e. ~P X |-> |^| { y e. ( Clsd ` J ) | x C_ y } ) )
8		elpwi	|- ( y e. ~P X -> y C_ X )
9	1	clscld	|- ( ( J e. Top /\ y C_ X ) -> ( ( cls ` J ) ` y ) e. ( Clsd ` J ) )
10	8 9	sylan2	|- ( ( J e. Top /\ y e. ~P X ) -> ( ( cls ` J ) ` y ) e. ( Clsd ` J ) )
11	6 7 10	fmpt2d	|- ( J e. Top -> ( cls ` J ) : ~P X --> ( Clsd ` J ) )