Metamath Proof Explorer

Theorem innei

Description: The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property V_ii of BourbakiTop1 p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006)

Ref Expression
Assertion innei 
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) -> ( N i^i M ) e. ( ( nei ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 neii1 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ U. J )
3 ssinss1 
 |-  ( N C_ U. J -> ( N i^i M ) C_ U. J )
4 2 3 syl 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> ( N i^i M ) C_ U. J )
5 4 3adant3 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) -> ( N i^i M ) C_ U. J )
6 neii2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. h e. J ( S C_ h /\ h C_ N ) )
7 neii2 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` S ) ) -> E. v e. J ( S C_ v /\ v C_ M ) )
8 6 7 anim12dan 
 |-  ( ( J e. Top /\ ( N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) ) -> ( E. h e. J ( S C_ h /\ h C_ N ) /\ E. v e. J ( S C_ v /\ v C_ M ) ) )
9 inopn 
 |-  ( ( J e. Top /\ h e. J /\ v e. J ) -> ( h i^i v ) e. J )
10 9 3expa 
 |-  ( ( ( J e. Top /\ h e. J ) /\ v e. J ) -> ( h i^i v ) e. J )
11 ssin 
 |-  ( ( S C_ h /\ S C_ v ) <-> S C_ ( h i^i v ) )
12 11 biimpi 
 |-  ( ( S C_ h /\ S C_ v ) -> S C_ ( h i^i v ) )
13 ss2in 
 |-  ( ( h C_ N /\ v C_ M ) -> ( h i^i v ) C_ ( N i^i M ) )
14 12 13 anim12i 
 |-  ( ( ( S C_ h /\ S C_ v ) /\ ( h C_ N /\ v C_ M ) ) -> ( S C_ ( h i^i v ) /\ ( h i^i v ) C_ ( N i^i M ) ) )
15 14 an4s 
 |-  ( ( ( S C_ h /\ h C_ N ) /\ ( S C_ v /\ v C_ M ) ) -> ( S C_ ( h i^i v ) /\ ( h i^i v ) C_ ( N i^i M ) ) )
16 sseq2 
 |-  ( g = ( h i^i v ) -> ( S C_ g <-> S C_ ( h i^i v ) ) )
17 sseq1 
 |-  ( g = ( h i^i v ) -> ( g C_ ( N i^i M ) <-> ( h i^i v ) C_ ( N i^i M ) ) )
18 16 17 anbi12d 
 |-  ( g = ( h i^i v ) -> ( ( S C_ g /\ g C_ ( N i^i M ) ) <-> ( S C_ ( h i^i v ) /\ ( h i^i v ) C_ ( N i^i M ) ) ) )
19 18 rspcev 
 |-  ( ( ( h i^i v ) e. J /\ ( S C_ ( h i^i v ) /\ ( h i^i v ) C_ ( N i^i M ) ) ) -> E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) )
20 10 15 19 syl2an 
 |-  ( ( ( ( J e. Top /\ h e. J ) /\ v e. J ) /\ ( ( S C_ h /\ h C_ N ) /\ ( S C_ v /\ v C_ M ) ) ) -> E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) )
21 20 expr 
 |-  ( ( ( ( J e. Top /\ h e. J ) /\ v e. J ) /\ ( S C_ h /\ h C_ N ) ) -> ( ( S C_ v /\ v C_ M ) -> E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) ) )
22 21 an32s 
 |-  ( ( ( ( J e. Top /\ h e. J ) /\ ( S C_ h /\ h C_ N ) ) /\ v e. J ) -> ( ( S C_ v /\ v C_ M ) -> E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) ) )
23 22 rexlimdva 
 |-  ( ( ( J e. Top /\ h e. J ) /\ ( S C_ h /\ h C_ N ) ) -> ( E. v e. J ( S C_ v /\ v C_ M ) -> E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) ) )
24 23 rexlimdva2 
 |-  ( J e. Top -> ( E. h e. J ( S C_ h /\ h C_ N ) -> ( E. v e. J ( S C_ v /\ v C_ M ) -> E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) ) ) )
25 24 imp32 
 |-  ( ( J e. Top /\ ( E. h e. J ( S C_ h /\ h C_ N ) /\ E. v e. J ( S C_ v /\ v C_ M ) ) ) -> E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) )
26 8 25 syldan 
 |-  ( ( J e. Top /\ ( N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) ) -> E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) )
27 26 3impb 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) )
28 1 neiss2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ U. J )
29 1 isnei 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( N i^i M ) e. ( ( nei ` J ) ` S ) <-> ( ( N i^i M ) C_ U. J /\ E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) ) ) )
30 28 29 syldan 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> ( ( N i^i M ) e. ( ( nei ` J ) ` S ) <-> ( ( N i^i M ) C_ U. J /\ E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) ) ) )
31 30 3adant3 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) -> ( ( N i^i M ) e. ( ( nei ` J ) ` S ) <-> ( ( N i^i M ) C_ U. J /\ E. g e. J ( S C_ g /\ g C_ ( N i^i M ) ) ) ) )
32 5 27 31 mpbir2and 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) -> ( N i^i M ) e. ( ( nei ` J ) ` S ) )