Metamath Proof Explorer

Theorem mvhf

Description: The function mapping variables to variable expressions is a function. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mvhf.v 
|- V = ( mVR ` T )
mvhf.e 
|- E = ( mEx ` T )
mvhf.h 
|- H = ( mVH ` T )
Assertion mvhf 
|- ( T e. mFS -> H : V --> E )

Proof

Step Hyp Ref Expression
1 mvhf.v 
 |-  V = ( mVR ` T )
2 mvhf.e 
 |-  E = ( mEx ` T )
3 mvhf.h 
 |-  H = ( mVH ` T )
4 eqid 
 |-  ( mTC ` T ) = ( mTC ` T )
5 eqid 
 |-  ( mType ` T ) = ( mType ` T )
6 1 4 5 mtyf2 
 |-  ( T e. mFS -> ( mType ` T ) : V --> ( mTC ` T ) )
7 6 ffvelrnda 
 |-  ( ( T e. mFS /\ v e. V ) -> ( ( mType ` T ) ` v ) e. ( mTC ` T ) )
8 elun2 
 |-  ( v e. V -> v e. ( ( mCN ` T ) u. V ) )
9 8 adantl 
 |-  ( ( T e. mFS /\ v e. V ) -> v e. ( ( mCN ` T ) u. V ) )
10 9 s1cld 
 |-  ( ( T e. mFS /\ v e. V ) -> <" v "> e. Word ( ( mCN ` T ) u. V ) )
11 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
12 eqid 
 |-  ( mREx ` T ) = ( mREx ` T )
13 11 1 12 mrexval 
 |-  ( T e. mFS -> ( mREx ` T ) = Word ( ( mCN ` T ) u. V ) )
14 13 adantr 
 |-  ( ( T e. mFS /\ v e. V ) -> ( mREx ` T ) = Word ( ( mCN ` T ) u. V ) )
15 10 14 eleqtrrd 
 |-  ( ( T e. mFS /\ v e. V ) -> <" v "> e. ( mREx ` T ) )
16 opelxpi 
 |-  ( ( ( ( mType ` T ) ` v ) e. ( mTC ` T ) /\ <" v "> e. ( mREx ` T ) ) -> <. ( ( mType ` T ) ` v ) , <" v "> >. e. ( ( mTC ` T ) X. ( mREx ` T ) ) )
17 7 15 16 syl2anc 
 |-  ( ( T e. mFS /\ v e. V ) -> <. ( ( mType ` T ) ` v ) , <" v "> >. e. ( ( mTC ` T ) X. ( mREx ` T ) ) )
18 4 2 12 mexval 
 |-  E = ( ( mTC ` T ) X. ( mREx ` T ) )
19 17 18 eleqtrrdi 
 |-  ( ( T e. mFS /\ v e. V ) -> <. ( ( mType ` T ) ` v ) , <" v "> >. e. E )
20 1 5 3 mvhfval 
 |-  H = ( v e. V |-> <. ( ( mType ` T ) ` v ) , <" v "> >. )
21 19 20 fmptd 
 |-  ( T e. mFS -> H : V --> E )