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

Metamath Proof Explorer

Theorem isnei

Description: The predicate "the class N is a neighborhood of S ". (Contributed by FL, 25-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis neifval.1 
|- X = U. J
Assertion isnei 
|- ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )

Proof

Step Hyp Ref Expression
1 neifval.1 
 |-  X = U. J
2 1 neival 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )
3 2 eleq2d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> N e. { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } ) )
4 sseq2 
 |-  ( v = N -> ( g C_ v <-> g C_ N ) )
5 4 anbi2d 
 |-  ( v = N -> ( ( S C_ g /\ g C_ v ) <-> ( S C_ g /\ g C_ N ) ) )
6 5 rexbidv 
 |-  ( v = N -> ( E. g e. J ( S C_ g /\ g C_ v ) <-> E. g e. J ( S C_ g /\ g C_ N ) ) )
7 6 elrab 
 |-  ( N e. { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } <-> ( N e. ~P X /\ E. g e. J ( S C_ g /\ g C_ N ) ) )
8 1 topopn 
 |-  ( J e. Top -> X e. J )
9 elpw2g 
 |-  ( X e. J -> ( N e. ~P X <-> N C_ X ) )
10 8 9 syl 
 |-  ( J e. Top -> ( N e. ~P X <-> N C_ X ) )
11 10 anbi1d 
 |-  ( J e. Top -> ( ( N e. ~P X /\ E. g e. J ( S C_ g /\ g C_ N ) ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
12 7 11 bitrid 
 |-  ( J e. Top -> ( N e. { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
13 12 adantr 
 |-  ( ( J e. Top /\ S C_ X ) -> ( N e. { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
14 3 13 bitrd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )