Theorem lpfval

Description: The limit point function on the subsets of a topology's base set. (Contributed by NM, 10-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Hypothesis	lpfval.1	|- X = U. J
Assertion	lpfval	|- ( J e. Top -> ( limPt ` J ) = ( x e. ~P X |-> { y | y e. ( ( cls ` J ) ` ( x \ { y } ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		lpfval.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 | y e. ( ( cls ` J ) ` ( x \ { y } ) ) } ) e. _V )
5	2 3 4	3syl	|- ( J e. Top -> ( x e. ~P X |-> { y | y e. ( ( cls ` J ) ` ( x \ { 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 -> ( cls ` j ) = ( cls ` J ) )
10	9	fveq1d	|- ( j = J -> ( ( cls ` j ) ` ( x \ { y } ) ) = ( ( cls ` J ) ` ( x \ { y } ) ) )
11	10	eleq2d	|- ( j = J -> ( y e. ( ( cls ` j ) ` ( x \ { y } ) ) <-> y e. ( ( cls ` J ) ` ( x \ { y } ) ) ) )
12	11	abbidv	|- ( j = J -> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } = { y | y e. ( ( cls ` J ) ` ( x \ { y } ) ) } )
13	8 12	mpteq12dv	|- ( j = J -> ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } ) = ( x e. ~P X |-> { y | y e. ( ( cls ` J ) ` ( x \ { y } ) ) } ) )
14		df-lp	|- limPt = ( j e. Top |-> ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } ) )
15	13 14	fvmptg	|- ( ( J e. Top /\ ( x e. ~P X |-> { y | y e. ( ( cls ` J ) ` ( x \ { y } ) ) } ) e. _V ) -> ( limPt ` J ) = ( x e. ~P X |-> { y | y e. ( ( cls ` J ) ` ( x \ { y } ) ) } ) )
16	5 15	mpdan	|- ( J e. Top -> ( limPt ` J ) = ( x e. ~P X |-> { y | y e. ( ( cls ` J ) ` ( x \ { y } ) ) } ) )