Description: The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | neifval.1 | |- X = U. J |
|
Assertion | neisspw | |- ( J e. Top -> ( ( nei ` J ) ` S ) C_ ~P X ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neifval.1 | |- X = U. J |
|
2 | 1 | neii1 | |- ( ( J e. Top /\ v e. ( ( nei ` J ) ` S ) ) -> v C_ X ) |
3 | velpw | |- ( v e. ~P X <-> v C_ X ) |
|
4 | 2 3 | sylibr | |- ( ( J e. Top /\ v e. ( ( nei ` J ) ` S ) ) -> v e. ~P X ) |
5 | 4 | ex | |- ( J e. Top -> ( v e. ( ( nei ` J ) ` S ) -> v e. ~P X ) ) |
6 | 5 | ssrdv | |- ( J e. Top -> ( ( nei ` J ) ` S ) C_ ~P X ) |