Theorem kur14lem2

Description: Lemma for kur14 . Write interior in terms of closure and complement: i A = c k c A where c is complement and k is closure. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	kur14lem.j	|- J e. Top
	kur14lem.x	|- X = U. J
	kur14lem.k	|- K = ( cls ` J )
	kur14lem.i	|- I = ( int ` J )
	kur14lem.a	|- A C_ X
Assertion	kur14lem2	|- ( I ` A ) = ( X \ ( K ` ( X \ A ) ) )

Proof

Step	Hyp	Ref	Expression
1		kur14lem.j	|- J e. Top
2		kur14lem.x	|- X = U. J
3		kur14lem.k	|- K = ( cls ` J )
4		kur14lem.i	|- I = ( int ` J )
5		kur14lem.a	|- A C_ X
6	2	ntrval2	|- ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` A ) = ( X \ ( ( cls ` J ) ` ( X \ A ) ) ) )
7	1 5 6	mp2an	|- ( ( int ` J ) ` A ) = ( X \ ( ( cls ` J ) ` ( X \ A ) ) )
8	4	fveq1i	|- ( I ` A ) = ( ( int ` J ) ` A )
9	3	fveq1i	|- ( K ` ( X \ A ) ) = ( ( cls ` J ) ` ( X \ A ) )
10	9	difeq2i	|- ( X \ ( K ` ( X \ A ) ) ) = ( X \ ( ( cls ` J ) ` ( X \ A ) ) )
11	7 8 10	3eqtr4i	|- ( I ` A ) = ( X \ ( K ` ( X \ A ) ) )