Metamath Proof Explorer

Theorem flimcls

Description: Closure in terms of filter convergence. (Contributed by Jeff Hankins, 28-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion flimcls 
|- ( ( J e. ( TopOn ` X ) /\ S C_ X ) -> ( A e. ( ( cls ` J ) ` S ) <-> E. f e. ( Fil ` X ) ( S e. f /\ A e. ( J fLim f ) ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) = ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) )
2 1 flimclslem 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) e. ( Fil ` X ) /\ S e. ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) ) )
3 3anass 
 |-  ( ( ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) e. ( Fil ` X ) /\ S e. ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) ) <-> ( ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) e. ( Fil ` X ) /\ ( S e. ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) ) ) )
4 2 3 sylib 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) e. ( Fil ` X ) /\ ( S e. ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) ) ) )
5 eleq2 
 |-  ( f = ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) -> ( S e. f <-> S e. ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) )
6 oveq2 
 |-  ( f = ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) -> ( J fLim f ) = ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) )
7 6 eleq2d 
 |-  ( f = ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) -> ( A e. ( J fLim f ) <-> A e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) ) )
8 5 7 anbi12d 
 |-  ( f = ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) -> ( ( S e. f /\ A e. ( J fLim f ) ) <-> ( S e. ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) ) ) )
9 8 rspcev 
 |-  ( ( ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) e. ( Fil ` X ) /\ ( S e. ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) ) ) -> E. f e. ( Fil ` X ) ( S e. f /\ A e. ( J fLim f ) ) )
10 4 9 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> E. f e. ( Fil ` X ) ( S e. f /\ A e. ( J fLim f ) ) )
11 10 3expia 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X ) -> ( A e. ( ( cls ` J ) ` S ) -> E. f e. ( Fil ` X ) ( S e. f /\ A e. ( J fLim f ) ) ) )
12 flimclsi 
 |-  ( S e. f -> ( J fLim f ) C_ ( ( cls ` J ) ` S ) )
13 12 sselda 
 |-  ( ( S e. f /\ A e. ( J fLim f ) ) -> A e. ( ( cls ` J ) ` S ) )
14 13 rexlimivw 
 |-  ( E. f e. ( Fil ` X ) ( S e. f /\ A e. ( J fLim f ) ) -> A e. ( ( cls ` J ) ` S ) )
15 11 14 impbid1 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X ) -> ( A e. ( ( cls ` J ) ` S ) <-> E. f e. ( Fil ` X ) ( S e. f /\ A e. ( J fLim f ) ) ) )