Theorem kur14lem3

Description: Lemma for kur14 . A closure is a subset of the base set. (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	kur14lem3	$$⊢K\left(A\right)\subseteq X$$

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	3	fveq1i	$$⊢K\left(A\right)=\mathrm{cls}\left(J\right)\left(A\right)$$
7	2	clsss3	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to \mathrm{cls}\left(J\right)\left(A\right)\subseteq X$$
8	1 5 7	mp2an	$$⊢\mathrm{cls}\left(J\right)\left(A\right)\subseteq X$$
9	6 8	eqsstri	$$⊢K\left(A\right)\subseteq X$$