Theorem kur14lem5

Description: Lemma for kur14 . Closure is an idempotent operation in the set of subsets of a topology. (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	kur14lem5	$$⊢K\left(K\left(A\right)\right)=K\left(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	clsidm	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to \mathrm{cls}\left(J\right)\left(\mathrm{cls}\left(J\right)\left(A\right)\right)=\mathrm{cls}\left(J\right)\left(A\right)$$
7	1 5 6	mp2an	$$⊢\mathrm{cls}\left(J\right)\left(\mathrm{cls}\left(J\right)\left(A\right)\right)=\mathrm{cls}\left(J\right)\left(A\right)$$
8	3	fveq1i	$$⊢K\left(A\right)=\mathrm{cls}\left(J\right)\left(A\right)$$
9	3 8	fveq12i	$$⊢K\left(K\left(A\right)\right)=\mathrm{cls}\left(J\right)\left(\mathrm{cls}\left(J\right)\left(A\right)\right)$$
10	7 9 8	3eqtr4i	$$⊢K\left(K\left(A\right)\right)=K\left(A\right)$$