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