Theorem clscld

Description: The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2	1	clsval	|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = |^| { x e. ( Clsd ` J ) | S C_ x } )
3	1	topcld	|- ( J e. Top -> X e. ( Clsd ` J ) )
4	3	anim1i	|- ( ( J e. Top /\ S C_ X ) -> ( X e. ( Clsd ` J ) /\ S C_ X ) )
5		sseq2	|- ( x = X -> ( S C_ x <-> S C_ X ) )
6	5	elrab	|- ( X e. { x e. ( Clsd ` J ) | S C_ x } <-> ( X e. ( Clsd ` J ) /\ S C_ X ) )
7	4 6	sylibr	|- ( ( J e. Top /\ S C_ X ) -> X e. { x e. ( Clsd ` J ) | S C_ x } )
8	7	ne0d	|- ( ( J e. Top /\ S C_ X ) -> { x e. ( Clsd ` J ) | S C_ x } =/= (/) )
9		ssrab2	|- { x e. ( Clsd ` J ) | S C_ x } C_ ( Clsd ` J )
10		intcld	|- ( ( { x e. ( Clsd ` J ) | S C_ x } =/= (/) /\ { x e. ( Clsd ` J ) | S C_ x } C_ ( Clsd ` J ) ) -> |^| { x e. ( Clsd ` J ) | S C_ x } e. ( Clsd ` J ) )
11	8 9 10	sylancl	|- ( ( J e. Top /\ S C_ X ) -> |^| { x e. ( Clsd ` J ) | S C_ x } e. ( Clsd ` J ) )
12	2 11	eqeltrd	|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )