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\in \mathrm{Top}$$
	kur14lem.x	$$⊢X=\bigcup J$$
	kur14lem.k	$$⊢K=\mathrm{cls}\left(J\right)$$
	kur14lem.i	$$⊢I=\mathrm{int}\left(J\right)$$
	kur14lem.a	$$⊢A\subseteq X$$
Assertion	kur14lem2	$$⊢I\left(A\right)=X\setminus K\left(X\setminus A\right)$$

Proof

Step	Hyp	Ref	Expression
1		kur14lem.j	$$⊢J\in \mathrm{Top}$$
2		kur14lem.x	$$⊢X=\bigcup J$$
3		kur14lem.k	$$⊢K=\mathrm{cls}\left(J\right)$$
4		kur14lem.i	$$⊢I=\mathrm{int}\left(J\right)$$
5		kur14lem.a	$$⊢A\subseteq X$$
6	2	ntrval2	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to \mathrm{int}\left(J\right)\left(A\right)=X\setminus \mathrm{cls}\left(J\right)\left(X\setminus A\right)$$
7	1 5 6	mp2an	$$⊢\mathrm{int}\left(J\right)\left(A\right)=X\setminus \mathrm{cls}\left(J\right)\left(X\setminus A\right)$$
8	4	fveq1i	$$⊢I\left(A\right)=\mathrm{int}\left(J\right)\left(A\right)$$
9	3	fveq1i	$$⊢K\left(X\setminus A\right)=\mathrm{cls}\left(J\right)\left(X\setminus A\right)$$
10	9	difeq2i	$$⊢X\setminus K\left(X\setminus A\right)=X\setminus \mathrm{cls}\left(J\right)\left(X\setminus A\right)$$
11	7 8 10	3eqtr4i	$$⊢I\left(A\right)=X\setminus K\left(X\setminus A\right)$$