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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) → 𝐽 ∈ Top )
2 1 3ad2ant1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → 𝐽 ∈ Top )
3 simp2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → 𝐴 ⊆ 𝑌 )
4 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐽 )
5 4 3ad2ant1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → 𝑌 = ∪ 𝐽 )
6 3 5 sseqtrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → 𝐴 ⊆ ∪ 𝐽 )
7 simp3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → 𝑃 ∈ 𝑌 )
8 7 5 eleqtrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → 𝑃 ∈ ∪ 𝐽 )
9 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
10 9 neindisj2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ∧ 𝑃 ∈ ∪ 𝐽 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑣 ∩ 𝐴 ) ≠ ∅ ) )
11 2 6 8 10 syl3anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑣 ∩ 𝐴 ) ≠ ∅ ) )
12 simp1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → 𝐽 ∈ ( TopOn ‘ 𝑌 ) )
13 7 snssd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → { 𝑃 } ⊆ 𝑌 )
14 snnzg ⊢ ( 𝑃 ∈ 𝑌 → { 𝑃 } ≠ ∅ )
15 14 3ad2ant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → { 𝑃 } ≠ ∅ )
16 neifil ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ { 𝑃 } ⊆ 𝑌 ∧ { 𝑃 } ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( Fil ‘ 𝑌 ) )
17 12 13 15 16 syl3anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( Fil ‘ 𝑌 ) )
18 trfil2 ⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑣 ∩ 𝐴 ) ≠ ∅ ) )
19 17 3 18 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑣 ∩ 𝐴 ) ≠ ∅ ) )
20 11 19 bitr4d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )