Metamath Proof Explorer

Theorem ntrval2

Description: Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007)

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

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ X = ⋃ J
2 difss ⊢ X ∖ S ⊆ X
3 1 clsval2 ⊢ J ∈ Top ∧ X ∖ S ⊆ X → cls ⁡ J ⁡ X ∖ S = X ∖ int ⁡ J ⁡ X ∖ X ∖ S
4 2 3 mpan2 ⊢ J ∈ Top → cls ⁡ J ⁡ X ∖ S = X ∖ int ⁡ J ⁡ X ∖ X ∖ S
5 4 adantr ⊢ J ∈ Top ∧ S ⊆ X → cls ⁡ J ⁡ X ∖ S = X ∖ int ⁡ J ⁡ X ∖ X ∖ S
6 dfss4 ⊢ S ⊆ X ↔ X ∖ X ∖ S = S
7 6 biimpi ⊢ S ⊆ X → X ∖ X ∖ S = S
8 7 fveq2d ⊢ S ⊆ X → int ⁡ J ⁡ X ∖ X ∖ S = int ⁡ J ⁡ S
9 8 adantl ⊢ J ∈ Top ∧ S ⊆ X → int ⁡ J ⁡ X ∖ X ∖ S = int ⁡ J ⁡ S
10 9 difeq2d ⊢ J ∈ Top ∧ S ⊆ X → X ∖ int ⁡ J ⁡ X ∖ X ∖ S = X ∖ int ⁡ J ⁡ S
11 5 10 eqtrd ⊢ J ∈ Top ∧ S ⊆ X → cls ⁡ J ⁡ X ∖ S = X ∖ int ⁡ J ⁡ S
12 11 difeq2d ⊢ J ∈ Top ∧ S ⊆ X → X ∖ cls ⁡ J ⁡ X ∖ S = X ∖ X ∖ int ⁡ J ⁡ S
13 1 ntropn ⊢ J ∈ Top ∧ S ⊆ X → int ⁡ J ⁡ S ∈ J
14 1 eltopss ⊢ J ∈ Top ∧ int ⁡ J ⁡ S ∈ J → int ⁡ J ⁡ S ⊆ X
15 13 14 syldan ⊢ J ∈ Top ∧ S ⊆ X → int ⁡ J ⁡ S ⊆ X
16 dfss4 ⊢ int ⁡ J ⁡ S ⊆ X ↔ X ∖ X ∖ int ⁡ J ⁡ S = int ⁡ J ⁡ S
17 15 16 sylib ⊢ J ∈ Top ∧ S ⊆ X → X ∖ X ∖ int ⁡ J ⁡ S = int ⁡ J ⁡ S
18 12 17 eqtr2d ⊢ J ∈ Top ∧ S ⊆ X → int ⁡ J ⁡ S = X ∖ cls ⁡ J ⁡ X ∖ S