Theorem mclsssv

Description: The closure of a set of expressions is a set of expressions. (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	mclsssv	|- ( ph -> ( K C B ) C_ E )

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		eqid	|- ( mAx ` T ) = ( mAx ` T )
9		eqid	|- ( mSubst ` T ) = ( mSubst ` T )
10		eqid	|- ( mVars ` T ) = ( mVars ` T )
11	1 2 3 4 5 6 7 8 9 10	mclsval	|- ( ph -> ( K C B ) = |^| { c | ( ( B u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
12	1 2 3 4 5 6 7 8 9 10	mclsssvlem	|- ( ph -> |^| { c | ( ( B u. ran ( mVH ` T ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` T ) -> A. s e. ran ( mSubst ` T ) ( ( ( s " ( o u. ran ( mVH ` T ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` x ) ) ) X. ( ( mVars ` T ) ` ( s ` ( ( mVH ` T ) ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ E )
13	11 12	eqsstrd	|- ( ph -> ( K C B ) C_ E )