Metamath Proof Explorer


Theorem neissex

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 J Top N nei J S x nei J S y y x N nei J y

Proof

Step Hyp Ref Expression
1 neii2 J Top N nei J S x J S x x N
2 opnneiss J Top x J S x x nei J S
3 2 3expb J Top x J S x x nei J S
4 3 adantrrr J Top x J S x x N x nei J S
5 4 adantlr J Top N nei J S x J S x x N x nei J S
6 simplll J Top N nei J S x J x N y x J Top
7 simpll J Top N nei J S x J J Top
8 simpr J Top N nei J S x J x J
9 eqid J = J
10 9 neii1 J Top N nei J S N J
11 10 adantr J Top N nei J S x J N J
12 9 opnssneib J Top x J N J x N N nei J x
13 7 8 11 12 syl3anc J Top N nei J S x J x N N nei J x
14 13 biimpa J Top N nei J S x J x N N nei J x
15 14 anasss J Top N nei J S x J x N N nei J x
16 15 adantr J Top N nei J S x J x N y x N nei J x
17 simpr J Top N nei J S x J x N y x y x
18 neiss J Top N nei J x y x N nei J y
19 6 16 17 18 syl3anc J Top N nei J S x J x N y x N nei J y
20 19 ex J Top N nei J S x J x N y x N nei J y
21 20 adantrrl J Top N nei J S x J S x x N y x N nei J y
22 21 alrimiv J Top N nei J S x J S x x N y y x N nei J y
23 1 5 22 reximssdv J Top N nei J S x nei J S y y x N nei J y