Theorem clsfval

Description: The closure function on the subsets of a topology's base set. (Contributed by NM, 3-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Hypothesis	cldval.1	|- X = U. J
Assertion	clsfval	|- ( J e. Top -> ( cls ` J ) = ( x e. ~P X |-> |^| { y e. ( Clsd ` J ) | x C_ y } ) )

Proof

Step	Hyp	Ref	Expression
1		cldval.1	|- X = U. J
2	1	topopn	|- ( J e. Top -> X e. J )
3		pwexg	|- ( X e. J -> ~P X e. _V )
4		mptexg	|- ( ~P X e. _V -> ( x e. ~P X |-> |^| { y e. ( Clsd ` J ) | x C_ y } ) e. _V )
5	2 3 4	3syl	|- ( J e. Top -> ( x e. ~P X |-> |^| { y e. ( Clsd ` J ) | x C_ y } ) e. _V )
6		unieq	|- ( j = J -> U. j = U. J )
7	6 1	eqtr4di	|- ( j = J -> U. j = X )
8	7	pweqd	|- ( j = J -> ~P U. j = ~P X )
9		fveq2	|- ( j = J -> ( Clsd ` j ) = ( Clsd ` J ) )
10	9	rabeqdv	|- ( j = J -> { y e. ( Clsd ` j ) | x C_ y } = { y e. ( Clsd ` J ) | x C_ y } )
11	10	inteqd	|- ( j = J -> |^| { y e. ( Clsd ` j ) | x C_ y } = |^| { y e. ( Clsd ` J ) | x C_ y } )
12	8 11	mpteq12dv	|- ( j = J -> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) = ( x e. ~P X |-> |^| { y e. ( Clsd ` J ) | x C_ y } ) )
13		df-cls	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
14	12 13	fvmptg	|- ( ( J e. Top /\ ( x e. ~P X |-> |^| { y e. ( Clsd ` J ) | x C_ y } ) e. _V ) -> ( cls ` J ) = ( x e. ~P X |-> |^| { y e. ( Clsd ` J ) | x C_ y } ) )
15	5 14	mpdan	|- ( J e. Top -> ( cls ` J ) = ( x e. ~P X |-> |^| { y e. ( Clsd ` J ) | x C_ y } ) )