Theorem iscld3

Description: A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006)

	Ref	Expression
Hypothesis	clscld.1	|- X = U. J
Assertion	iscld3	|- ( ( J e. Top /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( ( cls ` J ) ` S ) = S ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2		cldcls	|- ( S e. ( Clsd ` J ) -> ( ( cls ` J ) ` S ) = S )
3	1	clscld	|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )
4		eleq1	|- ( ( ( cls ` J ) ` S ) = S -> ( ( ( cls ` J ) ` S ) e. ( Clsd ` J ) <-> S e. ( Clsd ` J ) ) )
5	3 4	syl5ibcom	|- ( ( J e. Top /\ S C_ X ) -> ( ( ( cls ` J ) ` S ) = S -> S e. ( Clsd ` J ) ) )
6	2 5	impbid2	|- ( ( J e. Top /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( ( cls ` J ) ` S ) = S ) )