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

Theorem innei 19603
 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
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2443 . . . . 5
21neii1 19584 . . . 4
3 ssinss1 3711 . . . 4
42, 3syl 16 . . 3
6 neii2 19586 . . . . 5
7 neii2 19586 . . . . 5
86, 7anim12dan 837 . . . 4
9 inopn 19385 . . . . . . . . . . . 12
1093expa 1197 . . . . . . . . . . 11
11 ssin 3705 . . . . . . . . . . . . . 14
1211biimpi 194 . . . . . . . . . . . . 13
13 ss2in 3710 . . . . . . . . . . . . 13
1412, 13anim12i 566 . . . . . . . . . . . 12
1514an4s 826 . . . . . . . . . . 11
16 sseq2 3511 . . . . . . . . . . . . 13
17 sseq1 3510 . . . . . . . . . . . . 13
1816, 17anbi12d 710 . . . . . . . . . . . 12
1918rspcev 3196 . . . . . . . . . . 11
2010, 15, 19syl2an 477 . . . . . . . . . 10
2120expr 615 . . . . . . . . 9
2221an32s 804 . . . . . . . 8
2322rexlimdva 2935 . . . . . . 7
2423ex 434 . . . . . 6
2524rexlimdva 2935 . . . . 5
2625imp32 433 . . . 4
278, 26syldan 470 . . 3
28273impb 1193 . 2
291neiss2 19579 . . . 4
301isnei 19581 . . . 4
3129, 30syldan 470 . . 3