Metamath Proof Explorer


Theorem mtyf2

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

Ref Expression
Hypotheses mtyf2.v V = mVR T
mvtf2.k K = mTC T
mtyf2.y Y = mType T
Assertion mtyf2 T mFS Y : V K

Proof

Step Hyp Ref Expression
1 mtyf2.v V = mVR T
2 mvtf2.k K = mTC T
3 mtyf2.y Y = mType T
4 eqid mCN T = mCN T
5 eqid mVT T = mVT T
6 eqid mAx T = mAx T
7 eqid mStat T = mStat T
8 4 1 3 5 2 6 7 ismfs T mFS T mFS mCN T V = Y : V K mAx T mStat T v mVT T ¬ Y -1 v Fin
9 8 ibi T mFS mCN T V = Y : V K mAx T mStat T v mVT T ¬ Y -1 v Fin
10 9 simplrd T mFS Y : V K