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=\bigcup J$$
Assertion	fclselbas	$$⊢A\in \left(J\mathrm{fClus}F\right)\to A\in X$$

Proof

Step	Hyp	Ref	Expression
1		fclselbas.1	$$⊢X=\bigcup J$$
2	1	fclsfil	$$⊢A\in \left(J\mathrm{fClus}F\right)\to F\in \mathrm{Fil}\left(X\right)$$
3		fclstopon	$$⊢A\in \left(J\mathrm{fClus}F\right)\to \left(J\in \mathrm{TopOn}\left(X\right)\leftrightarrow F\in \mathrm{Fil}\left(X\right)\right)$$
4	2 3	mpbird	$$⊢A\in \left(J\mathrm{fClus}F\right)\to J\in \mathrm{TopOn}\left(X\right)$$
5		fclsopn	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge F\in \mathrm{Fil}\left(X\right)\right)\to \left(A\in \left(J\mathrm{fClus}F\right)\leftrightarrow \left(A\in X\wedge \forall o\in J\left(A\in o\to \forall s\in Fo\cap s\ne \varnothing \right)\right)\right)$$
6	4 2 5	syl2anc	$$⊢A\in \left(J\mathrm{fClus}F\right)\to \left(A\in \left(J\mathrm{fClus}F\right)\leftrightarrow \left(A\in X\wedge \forall o\in J\left(A\in o\to \forall s\in Fo\cap s\ne \varnothing \right)\right)\right)$$
7	6	ibi	$$⊢A\in \left(J\mathrm{fClus}F\right)\to \left(A\in X\wedge \forall o\in J\left(A\in o\to \forall s\in Fo\cap s\ne \varnothing \right)\right)$$
8	7	simpld	$$⊢A\in \left(J\mathrm{fClus}F\right)\to A\in X$$