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 JTopNneiJSxneiJSyyxNneiJy

Proof

Step Hyp Ref Expression
1 neii2 JTopNneiJSxJSxxN
2 opnneiss JTopxJSxxneiJS
3 2 3expb JTopxJSxxneiJS
4 3 adantrrr JTopxJSxxNxneiJS
5 4 adantlr JTopNneiJSxJSxxNxneiJS
6 simplll JTopNneiJSxJxNyxJTop
7 simpll JTopNneiJSxJJTop
8 simpr JTopNneiJSxJxJ
9 eqid J=J
10 9 neii1 JTopNneiJSNJ
11 10 adantr JTopNneiJSxJNJ
12 9 opnssneib JTopxJNJxNNneiJx
13 7 8 11 12 syl3anc JTopNneiJSxJxNNneiJx
14 13 biimpa JTopNneiJSxJxNNneiJx
15 14 anasss JTopNneiJSxJxNNneiJx
16 15 adantr JTopNneiJSxJxNyxNneiJx
17 simpr JTopNneiJSxJxNyxyx
18 neiss JTopNneiJxyxNneiJy
19 6 16 17 18 syl3anc JTopNneiJSxJxNyxNneiJy
20 19 ex JTopNneiJSxJxNyxNneiJy
21 20 adantrrl JTopNneiJSxJSxxNyxNneiJy
22 21 alrimiv JTopNneiJSxJSxxNyyxNneiJy
23 1 5 22 reximssdv JTopNneiJSxneiJSyyxNneiJy