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 e. Top /\ N C_ ( ( nei ` J ) ` S ) ) /\ ( N e. Fin /\ N =/= (/) ) ) -> |^| N e. ( ( nei ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( N C_ ( ( nei ` J ) ` S ) /\ ( N e. Fin /\ N =/= (/) ) ) -> N e. Fin )
2 innei 
 |-  ( ( J e. Top /\ x e. ( ( nei ` J ) ` S ) /\ y e. ( ( nei ` J ) ` S ) ) -> ( x i^i y ) e. ( ( nei ` J ) ` S ) )
3 2 3expib 
 |-  ( J e. Top -> ( ( x e. ( ( nei ` J ) ` S ) /\ y e. ( ( nei ` J ) ` S ) ) -> ( x i^i y ) e. ( ( nei ` J ) ` S ) ) )
4 3 ralrimivv 
 |-  ( J e. Top -> A. x e. ( ( nei ` J ) ` S ) A. y e. ( ( nei ` J ) ` S ) ( x i^i y ) e. ( ( nei ` J ) ` S ) )
5 fiint 
 |-  ( A. x e. ( ( nei ` J ) ` S ) A. y e. ( ( nei ` J ) ` S ) ( x i^i y ) e. ( ( nei ` J ) ` S ) <-> A. x ( ( x C_ ( ( nei ` J ) ` S ) /\ x =/= (/) /\ x e. Fin ) -> |^| x e. ( ( nei ` J ) ` S ) ) )
6 4 5 sylib 
 |-  ( J e. Top -> A. x ( ( x C_ ( ( nei ` J ) ` S ) /\ x =/= (/) /\ x e. Fin ) -> |^| x e. ( ( nei ` J ) ` S ) ) )
7 sseq1 
 |-  ( x = N -> ( x C_ ( ( nei ` J ) ` S ) <-> N C_ ( ( nei ` J ) ` S ) ) )
8 neeq1 
 |-  ( x = N -> ( x =/= (/) <-> N =/= (/) ) )
9 eleq1 
 |-  ( x = N -> ( x e. Fin <-> N e. Fin ) )
10 7 8 9 3anbi123d 
 |-  ( x = N -> ( ( x C_ ( ( nei ` J ) ` S ) /\ x =/= (/) /\ x e. Fin ) <-> ( N C_ ( ( nei ` J ) ` S ) /\ N =/= (/) /\ N e. Fin ) ) )
11 3ancomb 
 |-  ( ( N C_ ( ( nei ` J ) ` S ) /\ N =/= (/) /\ N e. Fin ) <-> ( N C_ ( ( nei ` J ) ` S ) /\ N e. Fin /\ N =/= (/) ) )
12 3anass 
 |-  ( ( N C_ ( ( nei ` J ) ` S ) /\ N e. Fin /\ N =/= (/) ) <-> ( N C_ ( ( nei ` J ) ` S ) /\ ( N e. Fin /\ N =/= (/) ) ) )
13 11 12 bitri 
 |-  ( ( N C_ ( ( nei ` J ) ` S ) /\ N =/= (/) /\ N e. Fin ) <-> ( N C_ ( ( nei ` J ) ` S ) /\ ( N e. Fin /\ N =/= (/) ) ) )
14 10 13 bitrdi 
 |-  ( x = N -> ( ( x C_ ( ( nei ` J ) ` S ) /\ x =/= (/) /\ x e. Fin ) <-> ( N C_ ( ( nei ` J ) ` S ) /\ ( N e. Fin /\ N =/= (/) ) ) ) )
15 inteq 
 |-  ( x = N -> |^| x = |^| N )
16 15 eleq1d 
 |-  ( x = N -> ( |^| x e. ( ( nei ` J ) ` S ) <-> |^| N e. ( ( nei ` J ) ` S ) ) )
17 14 16 imbi12d 
 |-  ( x = N -> ( ( ( x C_ ( ( nei ` J ) ` S ) /\ x =/= (/) /\ x e. Fin ) -> |^| x e. ( ( nei ` J ) ` S ) ) <-> ( ( N C_ ( ( nei ` J ) ` S ) /\ ( N e. Fin /\ N =/= (/) ) ) -> |^| N e. ( ( nei ` J ) ` S ) ) ) )
18 17 spcgv 
 |-  ( N e. Fin -> ( A. x ( ( x C_ ( ( nei ` J ) ` S ) /\ x =/= (/) /\ x e. Fin ) -> |^| x e. ( ( nei ` J ) ` S ) ) -> ( ( N C_ ( ( nei ` J ) ` S ) /\ ( N e. Fin /\ N =/= (/) ) ) -> |^| N e. ( ( nei ` J ) ` S ) ) ) )
19 6 18 syl5 
 |-  ( N e. Fin -> ( J e. Top -> ( ( N C_ ( ( nei ` J ) ` S ) /\ ( N e. Fin /\ N =/= (/) ) ) -> |^| N e. ( ( nei ` J ) ` S ) ) ) )
20 19 com3l 
 |-  ( J e. Top -> ( ( N C_ ( ( nei ` J ) ` S ) /\ ( N e. Fin /\ N =/= (/) ) ) -> ( N e. Fin -> |^| N e. ( ( nei ` J ) ` S ) ) ) )
21 1 20 mpdi 
 |-  ( J e. Top -> ( ( N C_ ( ( nei ` J ) ` S ) /\ ( N e. Fin /\ N =/= (/) ) ) -> |^| N e. ( ( nei ` J ) ` S ) ) )
22 21 impl 
 |-  ( ( ( J e. Top /\ N C_ ( ( nei ` J ) ` S ) ) /\ ( N e. Fin /\ N =/= (/) ) ) -> |^| N e. ( ( nei ` J ) ` S ) )