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	⊢ 𝑋 = ∪ 𝐽
Assertion	iscld	⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscld.1	⊢ 𝑋 = ∪ 𝐽
2	1	cldval	⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 } )
3	2	eleq2d	⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ 𝑆 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 } ) )
4		difeq2	⊢ ( 𝑥 = 𝑆 → ( 𝑋 ∖ 𝑥 ) = ( 𝑋 ∖ 𝑆 ) )
5	4	eleq1d	⊢ ( 𝑥 = 𝑆 → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 ↔ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) )
6	5	elrab	⊢ ( 𝑆 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 } ↔ ( 𝑆 ∈ 𝒫 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) )
7	3 6	bitrdi	⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆 ∈ 𝒫 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) )
8	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
9		elpw2g	⊢ ( 𝑋 ∈ 𝐽 → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
10	8 9	syl	⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
11	10	anbi1d	⊢ ( 𝐽 ∈ Top → ( ( 𝑆 ∈ 𝒫 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) )
12	7 11	bitrd	⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) )