Metamath Proof Explorer

Theorem difopn

Description: The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014)

Ref Expression
Hypothesis iscld.1 ⊢ X = ⋃ J
Assertion difopn ⊢ A ∈ J ∧ B ∈ Clsd ⁡ J → A ∖ B ∈ J

Proof

Step Hyp Ref Expression
1 iscld.1 ⊢ X = ⋃ J
2 elssuni ⊢ A ∈ J → A ⊆ ⋃ J
3 2 1 sseqtrrdi ⊢ A ∈ J → A ⊆ X
4 3 adantr ⊢ A ∈ J ∧ B ∈ Clsd ⁡ J → A ⊆ X
5 df-ss ⊢ A ⊆ X ↔ A ∩ X = A
6 4 5 sylib ⊢ A ∈ J ∧ B ∈ Clsd ⁡ J → A ∩ X = A
7 6 difeq1d ⊢ A ∈ J ∧ B ∈ Clsd ⁡ J → A ∩ X ∖ B = A ∖ B
8 indif2 ⊢ A ∩ X ∖ B = A ∩ X ∖ B
9 cldrcl ⊢ B ∈ Clsd ⁡ J → J ∈ Top
10 9 adantl ⊢ A ∈ J ∧ B ∈ Clsd ⁡ J → J ∈ Top
11 simpl ⊢ A ∈ J ∧ B ∈ Clsd ⁡ J → A ∈ J
12 1 cldopn ⊢ B ∈ Clsd ⁡ J → X ∖ B ∈ J
13 12 adantl ⊢ A ∈ J ∧ B ∈ Clsd ⁡ J → X ∖ B ∈ J
14 inopn ⊢ J ∈ Top ∧ A ∈ J ∧ X ∖ B ∈ J → A ∩ X ∖ B ∈ J
15 10 11 13 14 syl3anc ⊢ A ∈ J ∧ B ∈ Clsd ⁡ J → A ∩ X ∖ B ∈ J
16 8 15 eqeltrrid ⊢ A ∈ J ∧ B ∈ Clsd ⁡ J → A ∩ X ∖ B ∈ J
17 7 16 eqeltrrd ⊢ A ∈ J ∧ B ∈ Clsd ⁡ J → A ∖ B ∈ J