Metamath Proof Explorer

Theorem fcfelbas

Description: A cluster point of a function is in the base set of the topology. (Contributed by Jeff Hankins, 26-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion fcfelbas 
|- ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fClusf L ) ` F ) ) -> A e. X )

Proof

Step Hyp Ref Expression
1 fcfval 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( J fClus ( ( X FilMap F ) ` L ) ) )
2 1 eleq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) <-> A e. ( J fClus ( ( X FilMap F ) ` L ) ) ) )
3 eqid 
 |-  U. J = U. J
4 3 fclselbas 
 |-  ( A e. ( J fClus ( ( X FilMap F ) ` L ) ) -> A e. U. J )
5 2 4 biimtrdi 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) -> A e. U. J ) )
6 5 imp 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fClusf L ) ` F ) ) -> A e. U. J )
7 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fClusf L ) ` F ) ) -> J e. ( TopOn ` X ) )
8 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
9 7 8 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fClusf L ) ` F ) ) -> X = U. J )
10 6 9 eleqtrrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fClusf L ) ` F ) ) -> A e. X )