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 e. 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 e. mFS -> ( T e. mFS <-> ( ( ( ( mCN ` T ) i^i V ) = (/) /\ Y : V --> K ) /\ ( ( mAx ` T ) C_ ( mStat ` T ) /\ A. v e. ( mVT ` T ) -. ( `' Y " { v } ) e. Fin ) ) ) )
9 8 ibi 
 |-  ( T e. mFS -> ( ( ( ( mCN ` T ) i^i V ) = (/) /\ Y : V --> K ) /\ ( ( mAx ` T ) C_ ( mStat ` T ) /\ A. v e. ( mVT ` T ) -. ( `' Y " { v } ) e. Fin ) ) )
10 9 simplrd 
 |-  ( T e. mFS -> Y : V --> K )