Theorem opncld

Description: The complement of an open set is closed. (Contributed by NM, 6-Oct-2006)

	Ref	Expression
Hypothesis	iscld.1	⊢ 𝑋 = ∪ 𝐽
Assertion	opncld	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		iscld.1	⊢ 𝑋 = ∪ 𝐽
2		simpr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ∈ 𝐽 )
3	1	eltopss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ⊆ 𝑋 )
4	1	isopn2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐽 ↔ ( 𝑋 ∖ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) ) )
5	3 4	syldan	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → ( 𝑆 ∈ 𝐽 ↔ ( 𝑋 ∖ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) ) )
6	2 5	mpbid	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )