Theorem vhmcls

Description: All variable hypotheses are 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 )
	ssmclslem.h	|- H = ( mVH ` T )
	vhmcls.v	|- V = ( mVR ` T )
	vhmcls.3	|- ( ph -> X e. V )
Assertion	vhmcls	|- ( ph -> ( H ` X ) e. ( 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		ssmclslem.h	|- H = ( mVH ` T )
8		vhmcls.v	|- V = ( mVR ` T )
9		vhmcls.3	|- ( ph -> X e. V )
10	1 2 3 4 5 6 7	ssmclslem	|- ( ph -> ( B u. ran H ) C_ ( K C B ) )
11	10	unssbd	|- ( ph -> ran H C_ ( K C B ) )
12	8 2 7	mvhf	|- ( T e. mFS -> H : V --> E )
13		ffn	|- ( H : V --> E -> H Fn V )
14	4 12 13	3syl	|- ( ph -> H Fn V )
15		fnfvelrn	|- ( ( H Fn V /\ X e. V ) -> ( H ` X ) e. ran H )
16	14 9 15	syl2anc	|- ( ph -> ( H ` X ) e. ran H )
17	11 16	sseldd	|- ( ph -> ( H ` X ) e. ( K C B ) )