Metamath Proof Explorer

Theorem trnei

Description: The trace, over a set A , of the filter of the neighborhoods of a point P is a filter iff P belongs to the closure of A . (This is trfil2 applied to a filter of neighborhoods.) (Contributed by FL, 15-Sep-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion trnei ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → P ∈ cls ⁡ J ⁡ A ↔ nei ⁡ J ⁡ P ↾ 𝑡 A ∈ Fil ⁡ A

Proof

Step Hyp Ref Expression
1 topontop ⊢ J ∈ TopOn ⁡ Y → J ∈ Top
2 1 3ad2ant1 ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → J ∈ Top
3 simp2 ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → A ⊆ Y
4 toponuni ⊢ J ∈ TopOn ⁡ Y → Y = ⋃ J
5 4 3ad2ant1 ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → Y = ⋃ J
6 3 5 sseqtrd ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → A ⊆ ⋃ J
7 simp3 ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → P ∈ Y
8 7 5 eleqtrd ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → P ∈ ⋃ J
9 eqid ⊢ ⋃ J = ⋃ J
10 9 neindisj2 ⊢ J ∈ Top ∧ A ⊆ ⋃ J ∧ P ∈ ⋃ J → P ∈ cls ⁡ J ⁡ A ↔ ∀ v ∈ nei ⁡ J ⁡ P v ∩ A ≠ ∅
11 2 6 8 10 syl3anc ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → P ∈ cls ⁡ J ⁡ A ↔ ∀ v ∈ nei ⁡ J ⁡ P v ∩ A ≠ ∅
12 simp1 ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → J ∈ TopOn ⁡ Y
13 7 snssd ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → P ⊆ Y
14 snnzg ⊢ P ∈ Y → P ≠ ∅
15 14 3ad2ant3 ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → P ≠ ∅
16 neifil ⊢ J ∈ TopOn ⁡ Y ∧ P ⊆ Y ∧ P ≠ ∅ → nei ⁡ J ⁡ P ∈ Fil ⁡ Y
17 12 13 15 16 syl3anc ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → nei ⁡ J ⁡ P ∈ Fil ⁡ Y
18 trfil2 ⊢ nei ⁡ J ⁡ P ∈ Fil ⁡ Y ∧ A ⊆ Y → nei ⁡ J ⁡ P ↾ 𝑡 A ∈ Fil ⁡ A ↔ ∀ v ∈ nei ⁡ J ⁡ P v ∩ A ≠ ∅
19 17 3 18 syl2anc ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → nei ⁡ J ⁡ P ↾ 𝑡 A ∈ Fil ⁡ A ↔ ∀ v ∈ nei ⁡ J ⁡ P v ∩ A ≠ ∅
20 11 19 bitr4d ⊢ J ∈ TopOn ⁡ Y ∧ A ⊆ Y ∧ P ∈ Y → P ∈ cls ⁡ J ⁡ A ↔ nei ⁡ J ⁡ P ↾ 𝑡 A ∈ Fil ⁡ A