Theorem iscld

Description: The predicate "the class S is a closed set". (Contributed by NM, 2-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		iscld.1	|- X = U. J
2	1	cldval	|- ( J e. Top -> ( Clsd ` J ) = { x e. ~P X | ( X \ x ) e. J } )
3	2	eleq2d	|- ( J e. Top -> ( S e. ( Clsd ` J ) <-> S e. { x e. ~P X | ( X \ x ) e. J } ) )
4		difeq2	|- ( x = S -> ( X \ x ) = ( X \ S ) )
5	4	eleq1d	|- ( x = S -> ( ( X \ x ) e. J <-> ( X \ S ) e. J ) )
6	5	elrab	|- ( S e. { x e. ~P X | ( X \ x ) e. J } <-> ( S e. ~P X /\ ( X \ S ) e. J ) )
7	3 6	bitrdi	|- ( J e. Top -> ( S e. ( Clsd ` J ) <-> ( S e. ~P X /\ ( X \ S ) e. J ) ) )
8	1	topopn	|- ( J e. Top -> X e. J )
9		elpw2g	|- ( X e. J -> ( S e. ~P X <-> S C_ X ) )
10	8 9	syl	|- ( J e. Top -> ( S e. ~P X <-> S C_ X ) )
11	10	anbi1d	|- ( J e. Top -> ( ( S e. ~P X /\ ( X \ S ) e. J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) )
12	7 11	bitrd	|- ( J e. Top -> ( S e. ( Clsd ` J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) )