Theorem ntrdif

Description: An interior of a complement is the complement of the closure. This set is also known as the exterior of A . (Contributed by Jeff Hankins, 31-Aug-2009)

	Ref	Expression
Hypothesis	clscld.1	|- X = U. J
Assertion	ntrdif	|- ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` ( X \ A ) ) = ( X \ ( ( cls ` J ) ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2		difss	|- ( X \ A ) C_ X
3	1	ntrval2	|- ( ( J e. Top /\ ( X \ A ) C_ X ) -> ( ( int ` J ) ` ( X \ A ) ) = ( X \ ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) )
4	2 3	mpan2	|- ( J e. Top -> ( ( int ` J ) ` ( X \ A ) ) = ( X \ ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) )
5	4	adantr	|- ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` ( X \ A ) ) = ( X \ ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) )
6		simpr	|- ( ( J e. Top /\ A C_ X ) -> A C_ X )
7		dfss4	|- ( A C_ X <-> ( X \ ( X \ A ) ) = A )
8	6 7	sylib	|- ( ( J e. Top /\ A C_ X ) -> ( X \ ( X \ A ) ) = A )
9	8	fveq2d	|- ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) = ( ( cls ` J ) ` A ) )
10	9	difeq2d	|- ( ( J e. Top /\ A C_ X ) -> ( X \ ( ( cls ` J ) ` ( X \ ( X \ A ) ) ) ) = ( X \ ( ( cls ` J ) ` A ) ) )
11	5 10	eqtrd	|- ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` ( X \ A ) ) = ( X \ ( ( cls ` J ) ` A ) ) )