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 = J
Assertion fclselbas A J fClus F A X

Proof

Step Hyp Ref Expression
1 fclselbas.1 X = J
2 1 fclsfil A J fClus F F Fil X
3 fclstopon A J fClus F J TopOn X F Fil X
4 2 3 mpbird A J fClus F J TopOn X
5 fclsopn J TopOn X F Fil X A J fClus F A X o J A o s F o s
6 4 2 5 syl2anc A J fClus F A J fClus F A X o J A o s F o s
7 6 ibi A J fClus F A X o J A o s F o s
8 7 simpld A J fClus F A X