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	⊢ 𝐽 ∈ Top
	kur14lem.x	⊢ 𝑋 = ∪ 𝐽
	kur14lem.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
	kur14lem.i	⊢ 𝐼 = ( int ‘ 𝐽 )
	kur14lem.a	⊢ 𝐴 ⊆ 𝑋
Assertion	kur14lem2	⊢ ( 𝐼 ‘ 𝐴 ) = ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		kur14lem.j	⊢ 𝐽 ∈ Top
2		kur14lem.x	⊢ 𝑋 = ∪ 𝐽
3		kur14lem.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
4		kur14lem.i	⊢ 𝐼 = ( int ‘ 𝐽 )
5		kur14lem.a	⊢ 𝐴 ⊆ 𝑋
6	2	ntrval2	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ) )
7	1 5 6	mp2an	⊢ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) )
8	4	fveq1i	⊢ ( 𝐼 ‘ 𝐴 ) = ( ( int ‘ 𝐽 ) ‘ 𝐴 )
9	3	fveq1i	⊢ ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) )
10	9	difeq2i	⊢ ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) )
11	7 8 10	3eqtr4i	⊢ ( 𝐼 ‘ 𝐴 ) = ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) ) )