Theorem fclstopon

Description: Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		fclstop	$$⊢A\in \left(J\mathrm{fClus}F\right)\to J\in \mathrm{Top}$$
2		istopon	$$⊢J\in \mathrm{TopOn}\left(X\right)\leftrightarrow \left(J\in \mathrm{Top}\wedge X=\bigcup J\right)$$
3	2	baib	$$⊢J\in \mathrm{Top}\to \left(J\in \mathrm{TopOn}\left(X\right)\leftrightarrow X=\bigcup J\right)$$
4	1 3	syl	$$⊢A\in \left(J\mathrm{fClus}F\right)\to \left(J\in \mathrm{TopOn}\left(X\right)\leftrightarrow X=\bigcup J\right)$$
5		eqid	$$⊢\bigcup J=\bigcup J$$
6	5	fclsfil	$$⊢A\in \left(J\mathrm{fClus}F\right)\to F\in \mathrm{Fil}\left(\bigcup J\right)$$
7		fveq2	$$⊢X=\bigcup J\to \mathrm{Fil}\left(X\right)=\mathrm{Fil}\left(\bigcup J\right)$$
8	7	eleq2d	$$⊢X=\bigcup J\to \left(F\in \mathrm{Fil}\left(X\right)\leftrightarrow F\in \mathrm{Fil}\left(\bigcup J\right)\right)$$
9	6 8	syl5ibrcom	$$⊢A\in \left(J\mathrm{fClus}F\right)\to \left(X=\bigcup J\to F\in \mathrm{Fil}\left(X\right)\right)$$
10		filunibas	$$⊢F\in \mathrm{Fil}\left(\bigcup J\right)\to \bigcup F=\bigcup J$$
11	6 10	syl	$$⊢A\in \left(J\mathrm{fClus}F\right)\to \bigcup F=\bigcup J$$
12		filunibas	$$⊢F\in \mathrm{Fil}\left(X\right)\to \bigcup F=X$$
13	12	eqeq1d	$$⊢F\in \mathrm{Fil}\left(X\right)\to \left(\bigcup F=\bigcup J\leftrightarrow X=\bigcup J\right)$$
14	11 13	syl5ibcom	$$⊢A\in \left(J\mathrm{fClus}F\right)\to \left(F\in \mathrm{Fil}\left(X\right)\to X=\bigcup J\right)$$
15	9 14	impbid	$$⊢A\in \left(J\mathrm{fClus}F\right)\to \left(X=\bigcup J\leftrightarrow F\in \mathrm{Fil}\left(X\right)\right)$$
16	4 15	bitrd	$$⊢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)$$