Theorem fclsfil

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

Proof

Step	Hyp	Ref	Expression
1		fclsval.x	$$⊢X=\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(X\right)\wedge \forall s\in FA\in \mathrm{cls}\left(J\right)\left(s\right)\right)$$
3	2	simp2bi	$$⊢A\in \left(J\mathrm{fClus}F\right)\to F\in \mathrm{Fil}\left(X\right)$$