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=\mathrm{mVT}\left(T\right)$$
	mvtss.k	$$⊢K=\mathrm{mTC}\left(T\right)$$
Assertion	mvtss	$$⊢T\in \mathrm{mFS}\to F\subseteq K$$

Proof

Step	Hyp	Ref	Expression
1		mvtss.f	$$⊢F=\mathrm{mVT}\left(T\right)$$
2		mvtss.k	$$⊢K=\mathrm{mTC}\left(T\right)$$
3		eqid	$$⊢\mathrm{mType}\left(T\right)=\mathrm{mType}\left(T\right)$$
4	1 3	mvtval	$$⊢F=\mathrm{ran}\mathrm{mType}\left(T\right)$$
5		eqid	$$⊢\mathrm{mVR}\left(T\right)=\mathrm{mVR}\left(T\right)$$
6	5 2 3	mtyf2	$$⊢T\in \mathrm{mFS}\to \mathrm{mType}\left(T\right):\mathrm{mVR}\left(T\right)⟶K$$
7	6	frnd	$$⊢T\in \mathrm{mFS}\to \mathrm{ran}\mathrm{mType}\left(T\right)\subseteq K$$
8	4 7	eqsstrid	$$⊢T\in \mathrm{mFS}\to F\subseteq K$$