Description: For any neighborhood N of S , there is a neighborhood x of S such that N is a neighborhood of all subsets of x . Generalization to subsets of Property V_iv of BourbakiTop1 p. I.3. (Contributed by FL, 2-Oct-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | neissex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii2 | |
|
2 | opnneiss | |
|
3 | 2 | 3expb | |
4 | 3 | adantrrr | |
5 | 4 | adantlr | |
6 | simplll | |
|
7 | simpll | |
|
8 | simpr | |
|
9 | eqid | |
|
10 | 9 | neii1 | |
11 | 10 | adantr | |
12 | 9 | opnssneib | |
13 | 7 8 11 12 | syl3anc | |
14 | 13 | biimpa | |
15 | 14 | anasss | |
16 | 15 | adantr | |
17 | simpr | |
|
18 | neiss | |
|
19 | 6 16 17 18 | syl3anc | |
20 | 19 | ex | |
21 | 20 | adantrrl | |
22 | 21 | alrimiv | |
23 | 1 5 22 | reximssdv | |