Theorem mtyf

Description: The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mtyf.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
	mtyf.f	$$⊢F=\mathrm{mVT}\left(T\right)$$
	mtyf.y	$$⊢Y=\mathrm{mType}\left(T\right)$$
Assertion	mtyf	$$⊢T\in \mathrm{mFS}\to Y:V⟶F$$

Proof

Step	Hyp	Ref	Expression
1		mtyf.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
2		mtyf.f	$$⊢F=\mathrm{mVT}\left(T\right)$$
3		mtyf.y	$$⊢Y=\mathrm{mType}\left(T\right)$$
4		eqid	$$⊢\mathrm{mTC}\left(T\right)=\mathrm{mTC}\left(T\right)$$
5	1 4 3	mtyf2	$$⊢T\in \mathrm{mFS}\to Y:V⟶\mathrm{mTC}\left(T\right)$$
6		ffn	$$⊢Y:V⟶\mathrm{mTC}\left(T\right)\to YFnV$$
7		dffn4	$$⊢YFnV\leftrightarrow Y:V\underset{onto}{⟶}\mathrm{ran}Y$$
8	6 7	sylib	$$⊢Y:V⟶\mathrm{mTC}\left(T\right)\to Y:V\underset{onto}{⟶}\mathrm{ran}Y$$
9		fof	$$⊢Y:V\underset{onto}{⟶}\mathrm{ran}Y\to Y:V⟶\mathrm{ran}Y$$
10	5 8 9	3syl	$$⊢T\in \mathrm{mFS}\to Y:V⟶\mathrm{ran}Y$$
11	2 3	mvtval	$$⊢F=\mathrm{ran}Y$$
12		feq3	$$⊢F=\mathrm{ran}Y\to \left(Y:V⟶F\leftrightarrow Y:V⟶\mathrm{ran}Y\right)$$
13	11 12	ax-mp	$$⊢Y:V⟶F\leftrightarrow Y:V⟶\mathrm{ran}Y$$
14	10 13	sylibr	$$⊢T\in \mathrm{mFS}\to Y:V⟶F$$