Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  innei Unicode version

Theorem innei 12364
 Description: The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property Vii of [BourbakiTop1] p. I.3 for binary intersections. (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 2140 . . . . 5
21neii1 12348 . . . 4
3 ssinss1 3308 . . . 4
42, 3syl 14 . . 3
6 neii2 12350 . . . . 5
7 neii2 12350 . . . . 5
86, 7anim12dan 590 . . . 4
9 inopn 12202 . . . . . . . . . . 11
1093expa 1182 . . . . . . . . . 10
11 ssin 3301 . . . . . . . . . . . . 13
1211biimpi 119 . . . . . . . . . . . 12
13 ss2in 3307 . . . . . . . . . . . 12
1412, 13anim12i 336 . . . . . . . . . . 11
1514an4s 578 . . . . . . . . . 10
16 sseq2 3124 . . . . . . . . . . . 12
17 sseq1 3123 . . . . . . . . . . . 12
1816, 17anbi12d 465 . . . . . . . . . . 11
1918rspcev 2792 . . . . . . . . . 10
2010, 15, 19syl2an 287 . . . . . . . . 9
2120expr 373 . . . . . . . 8
2221an32s 558 . . . . . . 7
2322rexlimdva 2552 . . . . . 6
2423rexlimdva2 2555 . . . . 5
2524imp32 255 . . . 4
268, 25syldan 280 . . 3
27263impb 1178 . 2
281neiss2 12343 . . . 4
291isnei 12345 . . . 4
3028, 29syldan 280 . . 3