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 ( ( ( 𝐽 ∈ Top ∧ 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) → ∩ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) → 𝑁 ∈ Fin )
2 innei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
3 2 3expib ⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
4 3 ralrimivv ⊢ ( 𝐽 ∈ Top → ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ( 𝑥 ∩ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
5 fiint ⊢ ( ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ( 𝑥 ∩ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ( ( 𝑥 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
6 4 5 sylib ⊢ ( 𝐽 ∈ Top → ∀ 𝑥 ( ( 𝑥 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
7 sseq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
8 neeq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ≠ ∅ ↔ 𝑁 ≠ ∅ ) )
9 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ Fin ↔ 𝑁 ∈ Fin ) )
10 7 8 9 3anbi123d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) ↔ ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑁 ≠ ∅ ∧ 𝑁 ∈ Fin ) ) )
11 3ancomb ⊢ ( ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑁 ≠ ∅ ∧ 𝑁 ∈ Fin ) ↔ ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) )
12 3anass ⊢ ( ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ↔ ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) )
13 11 12 bitri ⊢ ( ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑁 ≠ ∅ ∧ 𝑁 ∈ Fin ) ↔ ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) )
14 10 13 bitrdi ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) ↔ ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) ) )
15 inteq ⊢ ( 𝑥 = 𝑁 → ∩ 𝑥 = ∩ 𝑁 )
16 15 eleq1d ⊢ ( 𝑥 = 𝑁 → ( ∩ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∩ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
17 14 16 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( ( 𝑥 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) → ∩ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
18 17 spcgv ⊢ ( 𝑁 ∈ Fin → ( ∀ 𝑥 ( ( 𝑥 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) → ∩ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
19 6 18 syl5 ⊢ ( 𝑁 ∈ Fin → ( 𝐽 ∈ Top → ( ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) → ∩ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
20 19 com3l ⊢ ( 𝐽 ∈ Top → ( ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) → ( 𝑁 ∈ Fin → ∩ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
21 1 20 mpdi ⊢ ( 𝐽 ∈ Top → ( ( 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) → ∩ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
22 21 impl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ⊆ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) ) → ∩ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )