Metamath Proof Explorer


Theorem neificl

Description: Neighborhoods are closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 25-Nov-2013)

Ref Expression
Assertion neificl J Top N nei J S N Fin N N nei J S

Proof

Step Hyp Ref Expression
1 simprl N nei J S N Fin N N Fin
2 innei J Top x nei J S y nei J S x y nei J S
3 2 3expib J Top x nei J S y nei J S x y nei J S
4 3 ralrimivv J Top x nei J S y nei J S x y nei J S
5 fiint x nei J S y nei J S x y nei J S x x nei J S x x Fin x nei J S
6 4 5 sylib J Top x x nei J S x x Fin x nei J S
7 sseq1 x = N x nei J S N nei J S
8 neeq1 x = N x N
9 eleq1 x = N x Fin N Fin
10 7 8 9 3anbi123d x = N x nei J S x x Fin N nei J S N N Fin
11 3ancomb N nei J S N N Fin N nei J S N Fin N
12 3anass N nei J S N Fin N N nei J S N Fin N
13 11 12 bitri N nei J S N N Fin N nei J S N Fin N
14 10 13 bitrdi x = N x nei J S x x Fin N nei J S N Fin N
15 inteq x = N x = N
16 15 eleq1d x = N x nei J S N nei J S
17 14 16 imbi12d x = N x nei J S x x Fin x nei J S N nei J S N Fin N N nei J S
18 17 spcgv N Fin x x nei J S x x Fin x nei J S N nei J S N Fin N N nei J S
19 6 18 syl5 N Fin J Top N nei J S N Fin N N nei J S
20 19 com3l J Top N nei J S N Fin N N Fin N nei J S
21 1 20 mpdi J Top N nei J S N Fin N N nei J S
22 21 impl J Top N nei J S N Fin N N nei J S