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 e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. x e. ( ( nei ` J ) ` S ) A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )

Proof

Step Hyp Ref Expression
1 neii2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. x e. J ( S C_ x /\ x C_ N ) )
2 opnneiss 
 |-  ( ( J e. Top /\ x e. J /\ S C_ x ) -> x e. ( ( nei ` J ) ` S ) )
3 2 3expb 
 |-  ( ( J e. Top /\ ( x e. J /\ S C_ x ) ) -> x e. ( ( nei ` J ) ` S ) )
4 3 adantrrr 
 |-  ( ( J e. Top /\ ( x e. J /\ ( S C_ x /\ x C_ N ) ) ) -> x e. ( ( nei ` J ) ` S ) )
5 4 adantlr 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ ( S C_ x /\ x C_ N ) ) ) -> x e. ( ( nei ` J ) ` S ) )
6 simplll 
 |-  ( ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) /\ y C_ x ) -> J e. Top )
7 simpll 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ x e. J ) -> J e. Top )
8 simpr 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ x e. J ) -> x e. J )
9 eqid 
 |-  U. J = U. J
10 9 neii1 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ U. J )
11 10 adantr 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ x e. J ) -> N C_ U. J )
12 9 opnssneib 
 |-  ( ( J e. Top /\ x e. J /\ N C_ U. J ) -> ( x C_ N <-> N e. ( ( nei ` J ) ` x ) ) )
13 7 8 11 12 syl3anc 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ x e. J ) -> ( x C_ N <-> N e. ( ( nei ` J ) ` x ) ) )
14 13 biimpa 
 |-  ( ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ x e. J ) /\ x C_ N ) -> N e. ( ( nei ` J ) ` x ) )
15 14 anasss 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) -> N e. ( ( nei ` J ) ` x ) )
16 15 adantr 
 |-  ( ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) /\ y C_ x ) -> N e. ( ( nei ` J ) ` x ) )
17 simpr 
 |-  ( ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) /\ y C_ x ) -> y C_ x )
18 neiss 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` x ) /\ y C_ x ) -> N e. ( ( nei ` J ) ` y ) )
19 6 16 17 18 syl3anc 
 |-  ( ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) /\ y C_ x ) -> N e. ( ( nei ` J ) ` y ) )
20 19 ex 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) -> ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )
21 20 adantrrl 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ ( S C_ x /\ x C_ N ) ) ) -> ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )
22 21 alrimiv 
 |-  ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ ( S C_ x /\ x C_ N ) ) ) -> A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )
23 1 5 22 reximssdv 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. x e. ( ( nei ` J ) ` S ) A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )