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 e. 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 e. 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 e. 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 e. mFS -> Y : V --> F )