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 Top M nei J A N nei J B M N nei J A B

Proof

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