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

Metamath Proof Explorer

Theorem neival

Description: Value of the set of neighborhoods of a subset of the base set of a topology. (Contributed by NM, 11-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis neifval.1 
|- X = U. J
Assertion neival 
|- ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )

Proof

Step Hyp Ref Expression
1 neifval.1 
 |-  X = U. J
2 1 neifval 
 |-  ( J e. Top -> ( nei ` J ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) )
3 2 fveq1d 
 |-  ( J e. Top -> ( ( nei ` J ) ` S ) = ( ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) ` S ) )
4 3 adantr 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = ( ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) ` S ) )
5 eqid 
 |-  ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } )
6 cleq1lem 
 |-  ( x = S -> ( ( x C_ g /\ g C_ v ) <-> ( S C_ g /\ g C_ v ) ) )
7 6 rexbidv 
 |-  ( x = S -> ( E. g e. J ( x C_ g /\ g C_ v ) <-> E. g e. J ( S C_ g /\ g C_ v ) ) )
8 7 rabbidv 
 |-  ( x = S -> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )
9 1 topopn 
 |-  ( J e. Top -> X e. J )
10 elpw2g 
 |-  ( X e. J -> ( S e. ~P X <-> S C_ X ) )
11 9 10 syl 
 |-  ( J e. Top -> ( S e. ~P X <-> S C_ X ) )
12 11 biimpar 
 |-  ( ( J e. Top /\ S C_ X ) -> S e. ~P X )
13 pwexg 
 |-  ( X e. J -> ~P X e. _V )
14 rabexg 
 |-  ( ~P X e. _V -> { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } e. _V )
15 9 13 14 3syl 
 |-  ( J e. Top -> { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } e. _V )
16 15 adantr 
 |-  ( ( J e. Top /\ S C_ X ) -> { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } e. _V )
17 5 8 12 16 fvmptd3 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )
18 4 17 eqtrd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )