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

Metamath Proof Explorer

Theorem ntrdif

Description: An interior of a complement is the complement of the closure. This set is also known as the exterior of A . (Contributed by Jeff Hankins, 31-Aug-2009)

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

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ X = ⋃ J
2 difss ⊢ X ∖ A ⊆ X
3 1 ntrval2 ⊢ J ∈ Top ∧ X ∖ A ⊆ X → int ⁡ J ⁡ X ∖ A = X ∖ cls ⁡ J ⁡ X ∖ X ∖ A
4 2 3 mpan2 ⊢ J ∈ Top → int ⁡ J ⁡ X ∖ A = X ∖ cls ⁡ J ⁡ X ∖ X ∖ A
5 4 adantr ⊢ J ∈ Top ∧ A ⊆ X → int ⁡ J ⁡ X ∖ A = X ∖ cls ⁡ 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 → cls ⁡ J ⁡ X ∖ X ∖ A = cls ⁡ J ⁡ A
10 9 difeq2d ⊢ J ∈ Top ∧ A ⊆ X → X ∖ cls ⁡ J ⁡ X ∖ X ∖ A = X ∖ cls ⁡ J ⁡ A
11 5 10 eqtrd ⊢ J ∈ Top ∧ A ⊆ X → int ⁡ J ⁡ X ∖ A = X ∖ cls ⁡ J ⁡ A