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 
|- 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 dfss2 
 |-  ( 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 )