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 ‘ 𝐴 ) ) )