This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> ( P e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { P } ) |`t A ) e. ( Fil ` A ) ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` Y ) -> J e. Top )
2 1 3ad2ant1 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> J e. Top )
3 simp2 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> A C_ Y )
4 toponuni 
 |-  ( J e. ( TopOn ` Y ) -> Y = U. J )
5 4 3ad2ant1 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> Y = U. J )
6 3 5 sseqtrd 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> A C_ U. J )
7 simp3 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> P e. Y )
8 7 5 eleqtrd 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> P e. U. J )
9 eqid 
 |-  U. J = U. J
10 9 neindisj2 
 |-  ( ( J e. Top /\ A C_ U. J /\ P e. U. J ) -> ( P e. ( ( cls ` J ) ` A ) <-> A. v e. ( ( nei ` J ) ` { P } ) ( v i^i A ) =/= (/) ) )
11 2 6 8 10 syl3anc 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> ( P e. ( ( cls ` J ) ` A ) <-> A. v e. ( ( nei ` J ) ` { P } ) ( v i^i A ) =/= (/) ) )
12 simp1 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> J e. ( TopOn ` Y ) )
13 7 snssd 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> { P } C_ Y )
14 snnzg 
 |-  ( P e. Y -> { P } =/= (/) )
15 14 3ad2ant3 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> { P } =/= (/) )
16 neifil 
 |-  ( ( J e. ( TopOn ` Y ) /\ { P } C_ Y /\ { P } =/= (/) ) -> ( ( nei ` J ) ` { P } ) e. ( Fil ` Y ) )
17 12 13 15 16 syl3anc 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> ( ( nei ` J ) ` { P } ) e. ( Fil ` Y ) )
18 trfil2 
 |-  ( ( ( ( nei ` J ) ` { P } ) e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( ( ( nei ` J ) ` { P } ) |`t A ) e. ( Fil ` A ) <-> A. v e. ( ( nei ` J ) ` { P } ) ( v i^i A ) =/= (/) ) )
19 17 3 18 syl2anc 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> ( ( ( ( nei ` J ) ` { P } ) |`t A ) e. ( Fil ` A ) <-> A. v e. ( ( nei ` J ) ` { P } ) ( v i^i A ) =/= (/) ) )
20 11 19 bitr4d 
 |-  ( ( J e. ( TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> ( P e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { P } ) |`t A ) e. ( Fil ` A ) ) )