Step |
Hyp |
Ref |
Expression |
1 |
|
neifval.1 |
|- X = U. J |
2 |
1
|
topopn |
|- ( J e. Top -> X e. J ) |
3 |
|
pwexg |
|- ( X e. J -> ~P X e. _V ) |
4 |
|
rabexg |
|- ( ~P X e. _V -> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } e. _V ) |
5 |
2 3 4
|
3syl |
|- ( J e. Top -> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } e. _V ) |
6 |
5
|
ralrimivw |
|- ( J e. Top -> A. x e. ~P X { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } e. _V ) |
7 |
|
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 ) } ) |
8 |
7
|
fnmpt |
|- ( A. x e. ~P X { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } e. _V -> ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) Fn ~P X ) |
9 |
6 8
|
syl |
|- ( J e. Top -> ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) Fn ~P X ) |
10 |
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 ) } ) ) |
11 |
10
|
fneq1d |
|- ( J e. Top -> ( ( nei ` J ) Fn ~P X <-> ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) Fn ~P X ) ) |
12 |
9 11
|
mpbird |
|- ( J e. Top -> ( nei ` J ) Fn ~P X ) |