Theorem mvtss

Description: The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mvtss.f	|- F = ( mVT ` T )
	mvtss.k	|- K = ( mTC ` T )
Assertion	mvtss	|- ( T e. mFS -> F C_ K )

Proof

Step	Hyp	Ref	Expression
1		mvtss.f	|- F = ( mVT ` T )
2		mvtss.k	|- K = ( mTC ` T )
3		eqid	|- ( mType ` T ) = ( mType ` T )
4	1 3	mvtval	|- F = ran ( mType ` T )
5		eqid	|- ( mVR ` T ) = ( mVR ` T )
6	5 2 3	mtyf2	|- ( T e. mFS -> ( mType ` T ) : ( mVR ` T ) --> K )
7	6	frnd	|- ( T e. mFS -> ran ( mType ` T ) C_ K )
8	4 7	eqsstrid	|- ( T e. mFS -> F C_ K )