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