Metamath Proof Explorer

Theorem cmclsopn

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

Ref Expression
Hypothesis clscld.1 ⊢ X = ⋃ J
Assertion cmclsopn ⊢ J ∈ Top ∧ S ⊆ X → X ∖ cls ⁡ J ⁡ S ∈ J

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ X = ⋃ J
2 1 clsval2 ⊢ J ∈ Top ∧ S ⊆ X → cls ⁡ J ⁡ S = X ∖ int ⁡ J ⁡ X ∖ S
3 2 difeq2d ⊢ J ∈ Top ∧ S ⊆ X → X ∖ cls ⁡ J ⁡ S = X ∖ X ∖ int ⁡ J ⁡ X ∖ S
4 difss ⊢ X ∖ S ⊆ X
5 1 ntropn ⊢ J ∈ Top ∧ X ∖ S ⊆ X → int ⁡ J ⁡ X ∖ S ∈ J
6 4 5 mpan2 ⊢ J ∈ Top → int ⁡ J ⁡ X ∖ S ∈ J
7 1 eltopss ⊢ J ∈ Top ∧ int ⁡ J ⁡ X ∖ S ∈ J → int ⁡ J ⁡ X ∖ S ⊆ X
8 6 7 mpdan ⊢ J ∈ Top → int ⁡ J ⁡ X ∖ S ⊆ X
9 dfss4 ⊢ int ⁡ J ⁡ X ∖ S ⊆ X ↔ X ∖ X ∖ int ⁡ J ⁡ X ∖ S = int ⁡ J ⁡ X ∖ S
10 8 9 sylib ⊢ J ∈ Top → X ∖ X ∖ int ⁡ J ⁡ X ∖ S = int ⁡ J ⁡ X ∖ S
11 10 6 eqeltrd ⊢ J ∈ Top → X ∖ X ∖ int ⁡ J ⁡ X ∖ S ∈ J
12 11 adantr ⊢ J ∈ Top ∧ S ⊆ X → X ∖ X ∖ int ⁡ J ⁡ X ∖ S ∈ J
13 3 12 eqeltrd ⊢ J ∈ Top ∧ S ⊆ X → X ∖ cls ⁡ J ⁡ S ∈ J