Theorem ssmcls

Description: The original expressions are also in the closure. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mclsval.d	$$⊢D=\mathrm{mDV}\left(T\right)$$
	mclsval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
	mclsval.c	$$⊢C=\mathrm{mCls}\left(T\right)$$
	mclsval.1	$$⊢\phi \to T\in \mathrm{mFS}$$
	mclsval.2	$$⊢\phi \to K\subseteq D$$
	mclsval.3	$$⊢\phi \to B\subseteq E$$
Assertion	ssmcls	$$⊢\phi \to B\subseteq KCB$$

Proof

Step	Hyp	Ref	Expression
1		mclsval.d	$$⊢D=\mathrm{mDV}\left(T\right)$$
2		mclsval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
3		mclsval.c	$$⊢C=\mathrm{mCls}\left(T\right)$$
4		mclsval.1	$$⊢\phi \to T\in \mathrm{mFS}$$
5		mclsval.2	$$⊢\phi \to K\subseteq D$$
6		mclsval.3	$$⊢\phi \to B\subseteq E$$
7		eqid	$$⊢\mathrm{mVH}\left(T\right)=\mathrm{mVH}\left(T\right)$$
8	1 2 3 4 5 6 7	ssmclslem	$$⊢\phi \to B\cup \mathrm{ran}\mathrm{mVH}\left(T\right)\subseteq KCB$$
9	8	unssad	$$⊢\phi \to B\subseteq KCB$$