Theorem ntrval2

Description: Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2		difss	|- ( X \ S ) C_ X
3	1	clsval2	|- ( ( J e. Top /\ ( X \ S ) C_ X ) -> ( ( cls ` J ) ` ( X \ S ) ) = ( X \ ( ( int ` J ) ` ( X \ ( X \ S ) ) ) ) )
4	2 3	mpan2	|- ( J e. Top -> ( ( cls ` J ) ` ( X \ S ) ) = ( X \ ( ( int ` J ) ` ( X \ ( X \ S ) ) ) ) )
5	4	adantr	|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` ( X \ S ) ) = ( X \ ( ( int ` J ) ` ( X \ ( X \ S ) ) ) ) )
6		dfss4	|- ( S C_ X <-> ( X \ ( X \ S ) ) = S )
7	6	biimpi	|- ( S C_ X -> ( X \ ( X \ S ) ) = S )
8	7	fveq2d	|- ( S C_ X -> ( ( int ` J ) ` ( X \ ( X \ S ) ) ) = ( ( int ` J ) ` S ) )
9	8	adantl	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` ( X \ ( X \ S ) ) ) = ( ( int ` J ) ` S ) )
10	9	difeq2d	|- ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( int ` J ) ` ( X \ ( X \ S ) ) ) ) = ( X \ ( ( int ` J ) ` S ) ) )
11	5 10	eqtrd	|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` ( X \ S ) ) = ( X \ ( ( int ` J ) ` S ) ) )
12	11	difeq2d	|- ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( cls ` J ) ` ( X \ S ) ) ) = ( X \ ( X \ ( ( int ` J ) ` S ) ) ) )
13	1	ntropn	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) e. J )
14	1	eltopss	|- ( ( J e. Top /\ ( ( int ` J ) ` S ) e. J ) -> ( ( int ` J ) ` S ) C_ X )
15	13 14	syldan	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) C_ X )
16		dfss4	|- ( ( ( int ` J ) ` S ) C_ X <-> ( X \ ( X \ ( ( int ` J ) ` S ) ) ) = ( ( int ` J ) ` S ) )
17	15 16	sylib	|- ( ( J e. Top /\ S C_ X ) -> ( X \ ( X \ ( ( int ` J ) ` S ) ) ) = ( ( int ` J ) ` S ) )
18	12 17	eqtr2d	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = ( X \ ( ( cls ` J ) ` ( X \ S ) ) ) )