Theorem clsdif

Description: A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2		difss	⊢ ( 𝑋 ∖ 𝐴 ) ⊆ 𝑋
3	1	clsval2	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝐴 ) ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) )
4	2 3	mpan2	⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) )
5	4	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) )
6		simpr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 )
7		dfss4	⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 )
8	6 7	sylib	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 )
9	8	fveq2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) = ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
10	9	difeq2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
11	5 10	eqtrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )