This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fclselbas

Description: A cluster point is in the base set. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis fclselbas.1 
|- X = U. J
Assertion fclselbas 
|- ( A e. ( J fClus F ) -> A e. X )

Proof

Step Hyp Ref Expression
1 fclselbas.1 
 |-  X = U. J
2 1 fclsfil 
 |-  ( A e. ( J fClus F ) -> F e. ( Fil ` X ) )
3 fclstopon 
 |-  ( A e. ( J fClus F ) -> ( J e. ( TopOn ` X ) <-> F e. ( Fil ` X ) ) )
4 2 3 mpbird 
 |-  ( A e. ( J fClus F ) -> J e. ( TopOn ` X ) )
5 fclsopn 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
6 4 2 5 syl2anc 
 |-  ( A e. ( J fClus F ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
7 6 ibi 
 |-  ( A e. ( J fClus F ) -> ( A e. X /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) )
8 7 simpld 
 |-  ( A e. ( J fClus F ) -> A e. X )