Theorem cmclsopn

Description: The complement of a closure is open. (Contributed by NM, 11-Sep-2006)

	Ref	Expression
Hypothesis	clscld.1	⊢ 𝑋 = ∪ 𝐽
Assertion	cmclsopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2	1	clsval2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) )
3	2	difeq2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) ) )
4		difss	⊢ ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋
5	1	ntropn	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ∈ 𝐽 )
6	4 5	mpan2	⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ∈ 𝐽 )
7	1	eltopss	⊢ ( ( 𝐽 ∈ Top ∧ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ⊆ 𝑋 )
8	6 7	mpdan	⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ⊆ 𝑋 )
9		dfss4	⊢ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) ) = ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) )
10	8 9	sylib	⊢ ( 𝐽 ∈ Top → ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) ) = ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) )
11	10 6	eqeltrd	⊢ ( 𝐽 ∈ Top → ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) ) ∈ 𝐽 )
12	11	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) ) ∈ 𝐽 )
13	3 12	eqeltrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ 𝐽 )