Theorem fclstop

Description: Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

	Ref	Expression
Assertion	fclstop	$$⊢A\in \left(J\mathrm{fClus}F\right)\to J\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup J=\bigcup J$$
2	1	isfcls	$$⊢A\in \left(J\mathrm{fClus}F\right)\leftrightarrow \left(J\in \mathrm{Top}\wedge F\in \mathrm{Fil}\left(\bigcup J\right)\wedge \forall s\in FA\in \mathrm{cls}\left(J\right)\left(s\right)\right)$$
3	2	simp1bi	$$⊢A\in \left(J\mathrm{fClus}F\right)\to J\in \mathrm{Top}$$