Theorem mtyf2

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

	Ref	Expression
Hypotheses	mtyf2.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
	mvtf2.k	$$⊢K=\mathrm{mTC}\left(T\right)$$
	mtyf2.y	$$⊢Y=\mathrm{mType}\left(T\right)$$
Assertion	mtyf2	$$⊢T\in \mathrm{mFS}\to Y:V⟶K$$

Proof

Step	Hyp	Ref	Expression
1		mtyf2.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
2		mvtf2.k	$$⊢K=\mathrm{mTC}\left(T\right)$$
3		mtyf2.y	$$⊢Y=\mathrm{mType}\left(T\right)$$
4		eqid	$$⊢\mathrm{mCN}\left(T\right)=\mathrm{mCN}\left(T\right)$$
5		eqid	$$⊢\mathrm{mVT}\left(T\right)=\mathrm{mVT}\left(T\right)$$
6		eqid	$$⊢\mathrm{mAx}\left(T\right)=\mathrm{mAx}\left(T\right)$$
7		eqid	$$⊢\mathrm{mStat}\left(T\right)=\mathrm{mStat}\left(T\right)$$
8	4 1 3 5 2 6 7	ismfs	$$⊢T\in \mathrm{mFS}\to \left(T\in \mathrm{mFS}\leftrightarrow \left(\left(\mathrm{mCN}\left(T\right)\cap V=\varnothing \wedge Y:V⟶K\right)\wedge \left(\mathrm{mAx}\left(T\right)\subseteq \mathrm{mStat}\left(T\right)\wedge \forall v\in \mathrm{mVT}\left(T\right)\neg Y^{-1}\left[\left\{v\right\}\right]\in \mathrm{Fin}\right)\right)\right)$$
9	8	ibi	$$⊢T\in \mathrm{mFS}\to \left(\left(\mathrm{mCN}\left(T\right)\cap V=\varnothing \wedge Y:V⟶K\right)\wedge \left(\mathrm{mAx}\left(T\right)\subseteq \mathrm{mStat}\left(T\right)\wedge \forall v\in \mathrm{mVT}\left(T\right)\neg Y^{-1}\left[\left\{v\right\}\right]\in \mathrm{Fin}\right)\right)$$
10	9	simplrd	$$⊢T\in \mathrm{mFS}\to Y:V⟶K$$