Step |
Hyp |
Ref |
Expression |
1 |
|
neifval.1 |
|- X = U. J |
2 |
|
elfvdm |
|- ( N e. ( ( nei ` J ) ` S ) -> S e. dom ( nei ` J ) ) |
3 |
2
|
adantl |
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S e. dom ( nei ` J ) ) |
4 |
1
|
neif |
|- ( J e. Top -> ( nei ` J ) Fn ~P X ) |
5 |
4
|
fndmd |
|- ( J e. Top -> dom ( nei ` J ) = ~P X ) |
6 |
5
|
eleq2d |
|- ( J e. Top -> ( S e. dom ( nei ` J ) <-> S e. ~P X ) ) |
7 |
6
|
adantr |
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> ( S e. dom ( nei ` J ) <-> S e. ~P X ) ) |
8 |
3 7
|
mpbid |
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S e. ~P X ) |
9 |
8
|
elpwid |
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ X ) |