This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ X = ⋃ J
Assertion clsdif ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ X ∖ A = X ∖ int ⁡ J ⁡ A

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ X = ⋃ J
2 difss ⊢ X ∖ A ⊆ X
3 1 clsval2 ⊢ J ∈ Top ∧ X ∖ A ⊆ X → cls ⁡ J ⁡ X ∖ A = X ∖ int ⁡ J ⁡ X ∖ X ∖ A
4 2 3 mpan2 ⊢ J ∈ Top → cls ⁡ J ⁡ X ∖ A = X ∖ int ⁡ J ⁡ X ∖ X ∖ A
5 4 adantr ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ X ∖ A = X ∖ int ⁡ J ⁡ X ∖ X ∖ A
6 simpr ⊢ J ∈ Top ∧ A ⊆ X → A ⊆ X
7 dfss4 ⊢ A ⊆ X ↔ X ∖ X ∖ A = A
8 6 7 sylib ⊢ J ∈ Top ∧ A ⊆ X → X ∖ X ∖ A = A
9 8 fveq2d ⊢ J ∈ Top ∧ A ⊆ X → int ⁡ J ⁡ X ∖ X ∖ A = int ⁡ J ⁡ A
10 9 difeq2d ⊢ J ∈ Top ∧ A ⊆ X → X ∖ int ⁡ J ⁡ X ∖ X ∖ A = X ∖ int ⁡ J ⁡ A
11 5 10 eqtrd ⊢ J ∈ Top ∧ A ⊆ X → cls ⁡ J ⁡ X ∖ A = X ∖ int ⁡ J ⁡ A