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 )