Metamath Proof Explorer

Theorem fclstopon

Description: Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion fclstopon 
|- ( A e. ( J fClus F ) -> ( J e. ( TopOn ` X ) <-> F e. ( Fil ` X ) ) )

Proof

Step Hyp Ref Expression
1 fclstop 
 |-  ( A e. ( J fClus F ) -> J e. Top )
2 istopon 
 |-  ( J e. ( TopOn ` X ) <-> ( J e. Top /\ X = U. J ) )
3 2 baib 
 |-  ( J e. Top -> ( J e. ( TopOn ` X ) <-> X = U. J ) )
4 1 3 syl 
 |-  ( A e. ( J fClus F ) -> ( J e. ( TopOn ` X ) <-> X = U. J ) )
5 eqid 
 |-  U. J = U. J
6 5 fclsfil 
 |-  ( A e. ( J fClus F ) -> F e. ( Fil ` U. J ) )
7 fveq2 
 |-  ( X = U. J -> ( Fil ` X ) = ( Fil ` U. J ) )
8 7 eleq2d 
 |-  ( X = U. J -> ( F e. ( Fil ` X ) <-> F e. ( Fil ` U. J ) ) )
9 6 8 syl5ibrcom 
 |-  ( A e. ( J fClus F ) -> ( X = U. J -> F e. ( Fil ` X ) ) )
10 filunibas 
 |-  ( F e. ( Fil ` U. J ) -> U. F = U. J )
11 6 10 syl 
 |-  ( A e. ( J fClus F ) -> U. F = U. J )
12 filunibas 
 |-  ( F e. ( Fil ` X ) -> U. F = X )
13 12 eqeq1d 
 |-  ( F e. ( Fil ` X ) -> ( U. F = U. J <-> X = U. J ) )
14 11 13 syl5ibcom 
 |-  ( A e. ( J fClus F ) -> ( F e. ( Fil ` X ) -> X = U. J ) )
15 9 14 impbid 
 |-  ( A e. ( J fClus F ) -> ( X = U. J <-> F e. ( Fil ` X ) ) )
16 4 15 bitrd 
 |-  ( A e. ( J fClus F ) -> ( J e. ( TopOn ` X ) <-> F e. ( Fil ` X ) ) )