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 syl5bb
 |-  ( 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 ) ) ) )