Theorem ssmcls

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

	Ref	Expression
Hypotheses	mclsval.d	|- D = ( mDV ` T )
	mclsval.e	|- E = ( mEx ` T )
	mclsval.c	|- C = ( mCls ` T )
	mclsval.1	|- ( ph -> T e. mFS )
	mclsval.2	|- ( ph -> K C_ D )
	mclsval.3	|- ( ph -> B C_ E )
Assertion	ssmcls	|- ( ph -> B C_ ( K C B ) )

Proof

Step	Hyp	Ref	Expression
1		mclsval.d	|- D = ( mDV ` T )
2		mclsval.e	|- E = ( mEx ` T )
3		mclsval.c	|- C = ( mCls ` T )
4		mclsval.1	|- ( ph -> T e. mFS )
5		mclsval.2	|- ( ph -> K C_ D )
6		mclsval.3	|- ( ph -> B C_ E )
7		eqid	|- ( mVH ` T ) = ( mVH ` T )
8	1 2 3 4 5 6 7	ssmclslem	|- ( ph -> ( B u. ran ( mVH ` T ) ) C_ ( K C B ) )
9	8	unssad	|- ( ph -> B C_ ( K C B ) )