# 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 𝑋 = 𝐽
Assertion difopn ( ( 𝐴𝐽𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴𝐵 ) ∈ 𝐽 )

### Proof

Step Hyp Ref Expression
1 iscld.1 𝑋 = 𝐽
2 elssuni ( 𝐴𝐽𝐴 𝐽 )
3 2 1 sseqtrrdi ( 𝐴𝐽𝐴𝑋 )
4 3 adantr ( ( 𝐴𝐽𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐴𝑋 )
5 df-ss ( 𝐴𝑋 ↔ ( 𝐴𝑋 ) = 𝐴 )
6 4 5 sylib ( ( 𝐴𝐽𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴𝑋 ) = 𝐴 )
7 6 difeq1d ( ( 𝐴𝐽𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝐴𝑋 ) ∖ 𝐵 ) = ( 𝐴𝐵 ) )
8 indif2 ( 𝐴 ∩ ( 𝑋𝐵 ) ) = ( ( 𝐴𝑋 ) ∖ 𝐵 )
9 cldrcl ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
10 9 adantl ( ( 𝐴𝐽𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐽 ∈ Top )
11 simpl ( ( 𝐴𝐽𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐴𝐽 )
12 1 cldopn ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋𝐵 ) ∈ 𝐽 )
13 12 adantl ( ( 𝐴𝐽𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋𝐵 ) ∈ 𝐽 )
14 inopn ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ∧ ( 𝑋𝐵 ) ∈ 𝐽 ) → ( 𝐴 ∩ ( 𝑋𝐵 ) ) ∈ 𝐽 )
15 10 11 13 14 syl3anc ( ( 𝐴𝐽𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴 ∩ ( 𝑋𝐵 ) ) ∈ 𝐽 )
16 8 15 eqeltrrid ( ( 𝐴𝐽𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝐴𝑋 ) ∖ 𝐵 ) ∈ 𝐽 )
17 7 16 eqeltrrd ( ( 𝐴𝐽𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴𝐵 ) ∈ 𝐽 )