Metamath Proof Explorer

Theorem isfcls2

Description: A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion isfcls2 
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> A. s e. F A e. ( ( cls ` J ) ` s ) ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
2 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
3 2 fveq2d 
 |-  ( J e. ( TopOn ` X ) -> ( Fil ` X ) = ( Fil ` U. J ) )
4 3 eleq2d 
 |-  ( J e. ( TopOn ` X ) -> ( F e. ( Fil ` X ) <-> F e. ( Fil ` U. J ) ) )
5 4 biimpa 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> F e. ( Fil ` U. J ) )
6 eqid 
 |-  U. J = U. J
7 6 isfcls 
 |-  ( A e. ( J fClus F ) <-> ( J e. Top /\ F e. ( Fil ` U. J ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )
8 df-3an 
 |-  ( ( J e. Top /\ F e. ( Fil ` U. J ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) <-> ( ( J e. Top /\ F e. ( Fil ` U. J ) ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )
9 7 8 bitri 
 |-  ( A e. ( J fClus F ) <-> ( ( J e. Top /\ F e. ( Fil ` U. J ) ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )
10 9 baib 
 |-  ( ( J e. Top /\ F e. ( Fil ` U. J ) ) -> ( A e. ( J fClus F ) <-> A. s e. F A e. ( ( cls ` J ) ` s ) ) )
11 1 5 10 syl2an2r 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> A. s e. F A e. ( ( cls ` J ) ` s ) ) )