This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) ) } ) )