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	⊢ 𝐹 = ( mVT ‘ 𝑇 )
	mvtss.k	⊢ 𝐾 = ( mTC ‘ 𝑇 )
Assertion	mvtss	⊢ ( 𝑇 ∈ mFS → 𝐹 ⊆ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		mvtss.f	⊢ 𝐹 = ( mVT ‘ 𝑇 )
2		mvtss.k	⊢ 𝐾 = ( mTC ‘ 𝑇 )
3		eqid	⊢ ( mType ‘ 𝑇 ) = ( mType ‘ 𝑇 )
4	1 3	mvtval	⊢ 𝐹 = ran ( mType ‘ 𝑇 )
5		eqid	⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
6	5 2 3	mtyf2	⊢ ( 𝑇 ∈ mFS → ( mType ‘ 𝑇 ) : ( mVR ‘ 𝑇 ) ⟶ 𝐾 )
7	6	frnd	⊢ ( 𝑇 ∈ mFS → ran ( mType ‘ 𝑇 ) ⊆ 𝐾 )
8	4 7	eqsstrid	⊢ ( 𝑇 ∈ mFS → 𝐹 ⊆ 𝐾 )