Metamath Proof Explorer

Theorem neiin

Description: Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) ) -> M e. ( ( nei ` J ) ` A ) )
2 simpl 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) ) -> J e. Top )
3 eqid 
 |-  U. J = U. J
4 3 neiss2 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) ) -> A C_ U. J )
5 3 neii1 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) ) -> M C_ U. J )
6 3 neiint 
 |-  ( ( J e. Top /\ A C_ U. J /\ M C_ U. J ) -> ( M e. ( ( nei ` J ) ` A ) <-> A C_ ( ( int ` J ) ` M ) ) )
7 2 4 5 6 syl3anc 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) ) -> ( M e. ( ( nei ` J ) ` A ) <-> A C_ ( ( int ` J ) ` M ) ) )
8 1 7 mpbid 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) ) -> A C_ ( ( int ` J ) ` M ) )
9 ssinss1 
 |-  ( A C_ ( ( int ` J ) ` M ) -> ( A i^i B ) C_ ( ( int ` J ) ` M ) )
10 8 9 syl 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) ) -> ( A i^i B ) C_ ( ( int ` J ) ` M ) )
11 10 3adant3 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> ( A i^i B ) C_ ( ( int ` J ) ` M ) )
12 inss2 
 |-  ( A i^i B ) C_ B
13 simpr 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` B ) ) -> N e. ( ( nei ` J ) ` B ) )
14 simpl 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` B ) ) -> J e. Top )
15 3 neiss2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` B ) ) -> B C_ U. J )
16 3 neii1 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` B ) ) -> N C_ U. J )
17 3 neiint 
 |-  ( ( J e. Top /\ B C_ U. J /\ N C_ U. J ) -> ( N e. ( ( nei ` J ) ` B ) <-> B C_ ( ( int ` J ) ` N ) ) )
18 14 15 16 17 syl3anc 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` B ) ) -> ( N e. ( ( nei ` J ) ` B ) <-> B C_ ( ( int ` J ) ` N ) ) )
19 13 18 mpbid 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` B ) ) -> B C_ ( ( int ` J ) ` N ) )
20 19 3adant2 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> B C_ ( ( int ` J ) ` N ) )
21 12 20 sstrid 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> ( A i^i B ) C_ ( ( int ` J ) ` N ) )
22 11 21 ssind 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> ( A i^i B ) C_ ( ( ( int ` J ) ` M ) i^i ( ( int ` J ) ` N ) ) )
23 simp1 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> J e. Top )
24 5 3adant3 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> M C_ U. J )
25 16 3adant2 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> N C_ U. J )
26 3 ntrin 
 |-  ( ( J e. Top /\ M C_ U. J /\ N C_ U. J ) -> ( ( int ` J ) ` ( M i^i N ) ) = ( ( ( int ` J ) ` M ) i^i ( ( int ` J ) ` N ) ) )
27 23 24 25 26 syl3anc 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> ( ( int ` J ) ` ( M i^i N ) ) = ( ( ( int ` J ) ` M ) i^i ( ( int ` J ) ` N ) ) )
28 22 27 sseqtrrd 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> ( A i^i B ) C_ ( ( int ` J ) ` ( M i^i N ) ) )
29 ssinss1 
 |-  ( A C_ U. J -> ( A i^i B ) C_ U. J )
30 4 29 syl 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) ) -> ( A i^i B ) C_ U. J )
31 ssinss1 
 |-  ( M C_ U. J -> ( M i^i N ) C_ U. J )
32 5 31 syl 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) ) -> ( M i^i N ) C_ U. J )
33 3 neiint 
 |-  ( ( J e. Top /\ ( A i^i B ) C_ U. J /\ ( M i^i N ) C_ U. J ) -> ( ( M i^i N ) e. ( ( nei ` J ) ` ( A i^i B ) ) <-> ( A i^i B ) C_ ( ( int ` J ) ` ( M i^i N ) ) ) )
34 2 30 32 33 syl3anc 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) ) -> ( ( M i^i N ) e. ( ( nei ` J ) ` ( A i^i B ) ) <-> ( A i^i B ) C_ ( ( int ` J ) ` ( M i^i N ) ) ) )
35 34 3adant3 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> ( ( M i^i N ) e. ( ( nei ` J ) ` ( A i^i B ) ) <-> ( A i^i B ) C_ ( ( int ` J ) ` ( M i^i N ) ) ) )
36 28 35 mpbird 
 |-  ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> ( M i^i N ) e. ( ( nei ` J ) ` ( A i^i B ) ) )