Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  innei Unicode version

Theorem innei 16694
 Description: The intersection of two neighborhoods of a set is also a neighborhood of the set. Proposition Vii of [BourbakiTop1] p. I.3 . (Contributed by FL, 28-Sep-2006.)
Assertion
Ref Expression
innei

Proof of Theorem innei
StepHypRef Expression
1 eqid 2253 . . . . 5
21neii1 16675 . . . 4
3 ssinss1 3304 . . . 4
42, 3syl 17 . . 3
6 neii2 16677 . . . . 5
7 neii2 16677 . . . . 5
86, 7anim12dan 813 . . . 4
9 inopn 16477 . . . . . . . . . . . 12
1093expa 1156 . . . . . . . . . . 11
11 ssin 3298 . . . . . . . . . . . . . 14
1211biimpi 188 . . . . . . . . . . . . 13
13 ss2in 3303 . . . . . . . . . . . . 13
1412, 13anim12i 551 . . . . . . . . . . . 12
1514an4s 802 . . . . . . . . . . 11
16 sseq2 3121 . . . . . . . . . . . . 13
17 sseq1 3120 . . . . . . . . . . . . 13
1816, 17anbi12d 694 . . . . . . . . . . . 12
1918rcla4ev 2821 . . . . . . . . . . 11
2010, 15, 19syl2an 465 . . . . . . . . . 10
2120expr 601 . . . . . . . . 9
2221an32s 782 . . . . . . . 8
2322rexlimdva 2629 . . . . . . 7
2423ex 425 . . . . . 6
2524rexlimdva 2629 . . . . 5
2625imp32 424 . . . 4
278, 26syldan 458 . . 3
28273impb 1152 . 2
291neiss2 16670 . . . 4
301isnei 16672 . . . 4
3129, 30syldan 458 . . 3