Metamath Proof Explorer


Theorem mvtval

Description: The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mvtval.f V = mVT T
mvtval.y Y = mType T
Assertion mvtval V = ran Y

Proof

Step Hyp Ref Expression
1 mvtval.f V = mVT T
2 mvtval.y Y = mType T
3 fveq2 t = T mType t = mType T
4 3 rneqd t = T ran mType t = ran mType T
5 df-mvt mVT = t V ran mType t
6 fvex mType T V
7 6 rnex ran mType T V
8 4 5 7 fvmpt T V mVT T = ran mType T
9 rn0 ran =
10 9 eqcomi = ran
11 fvprc ¬ T V mVT T =
12 fvprc ¬ T V mType T =
13 12 rneqd ¬ T V ran mType T = ran
14 10 11 13 3eqtr4a ¬ T V mVT T = ran mType T
15 8 14 pm2.61i mVT T = ran mType T
16 2 rneqi ran Y = ran mType T
17 15 1 16 3eqtr4i V = ran Y