This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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