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 e. _V |-> ran ( mType ` t ) )
6 fvex 
 |-  ( mType ` T ) e. _V
7 6 rnex 
 |-  ran ( mType ` T ) e. _V
8 4 5 7 fvmpt 
 |-  ( T e. _V -> ( mVT ` T ) = ran ( mType ` T ) )
9 rn0 
 |-  ran (/) = (/)
10 9 eqcomi 
 |-  (/) = ran (/)
11 fvprc 
 |-  ( -. T e. _V -> ( mVT ` T ) = (/) )
12 fvprc 
 |-  ( -. T e. _V -> ( mType ` T ) = (/) )
13 12 rneqd 
 |-  ( -. T e. _V -> ran ( mType ` T ) = ran (/) )
14 10 11 13 3eqtr4a 
 |-  ( -. T e. _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