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 = U. J
Assertion	difopn	|- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( A \ B ) e. J )

Proof

Step	Hyp	Ref	Expression
1		iscld.1	|- X = U. J
2		elssuni	|- ( A e. J -> A C_ U. J )
3	2 1	sseqtrrdi	|- ( A e. J -> A C_ X )
4	3	adantr	|- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> A C_ X )
5		df-ss	|- ( A C_ X <-> ( A i^i X ) = A )
6	4 5	sylib	|- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( A i^i X ) = A )
7	6	difeq1d	|- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( ( A i^i X ) \ B ) = ( A \ B ) )
8		indif2	|- ( A i^i ( X \ B ) ) = ( ( A i^i X ) \ B )
9		cldrcl	|- ( B e. ( Clsd ` J ) -> J e. Top )
10	9	adantl	|- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> J e. Top )
11		simpl	|- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> A e. J )
12	1	cldopn	|- ( B e. ( Clsd ` J ) -> ( X \ B ) e. J )
13	12	adantl	|- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( X \ B ) e. J )
14		inopn	|- ( ( J e. Top /\ A e. J /\ ( X \ B ) e. J ) -> ( A i^i ( X \ B ) ) e. J )
15	10 11 13 14	syl3anc	|- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( A i^i ( X \ B ) ) e. J )
16	8 15	eqeltrrid	|- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( ( A i^i X ) \ B ) e. J )
17	7 16	eqeltrrd	|- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( A \ B ) e. J )