Metamath Proof Explorer


Theorem mtyf

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

Ref Expression
Hypotheses mtyf.v V = mVR T
mtyf.f F = mVT T
mtyf.y Y = mType T
Assertion mtyf T mFS Y : V F

Proof

Step Hyp Ref Expression
1 mtyf.v V = mVR T
2 mtyf.f F = mVT T
3 mtyf.y Y = mType T
4 eqid mTC T = mTC T
5 1 4 3 mtyf2 T mFS Y : V mTC T
6 ffn Y : V mTC T Y Fn V
7 dffn4 Y Fn V Y : V onto ran Y
8 6 7 sylib Y : V mTC T Y : V onto ran Y
9 fof Y : V onto ran Y Y : V ran Y
10 5 8 9 3syl T mFS Y : V ran Y
11 2 3 mvtval F = ran Y
12 feq3 F = ran Y Y : V F Y : V ran Y
13 11 12 ax-mp Y : V F Y : V ran Y
14 10 13 sylibr T mFS Y : V F