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

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 dfss2 ⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝐴 ∩ 𝑋 ) = 𝐴 )
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 ‘ 𝐽 ) ) → ( 𝐴 ∖ 𝐵 ) ∈ 𝐽 )