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 ‘ 𝐽 ) ) → ( 𝐴 ∖ 𝐵 ) ∈ 𝐽 )