Theorem mvhfval

Description: Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mvhfval.v	|- V = ( mVR ` T )
	mvhfval.y	|- Y = ( mType ` T )
	mvhfval.h	|- H = ( mVH ` T )
Assertion	mvhfval	|- H = ( v e. V |-> <. ( Y ` v ) , <" v "> >. )

Proof

Step	Hyp	Ref	Expression
1		mvhfval.v	|- V = ( mVR ` T )
2		mvhfval.y	|- Y = ( mType ` T )
3		mvhfval.h	|- H = ( mVH ` T )
4		fveq2	|- ( t = T -> ( mVR ` t ) = ( mVR ` T ) )
5	4 1	eqtr4di	|- ( t = T -> ( mVR ` t ) = V )
6		fveq2	|- ( t = T -> ( mType ` t ) = ( mType ` T ) )
7	6 2	eqtr4di	|- ( t = T -> ( mType ` t ) = Y )
8	7	fveq1d	|- ( t = T -> ( ( mType ` t ) ` v ) = ( Y ` v ) )
9	8	opeq1d	|- ( t = T -> <. ( ( mType ` t ) ` v ) , <" v "> >. = <. ( Y ` v ) , <" v "> >. )
10	5 9	mpteq12dv	|- ( t = T -> ( v e. ( mVR ` t ) |-> <. ( ( mType ` t ) ` v ) , <" v "> >. ) = ( v e. V |-> <. ( Y ` v ) , <" v "> >. ) )
11		df-mvh	|- mVH = ( t e. _V |-> ( v e. ( mVR ` t ) |-> <. ( ( mType ` t ) ` v ) , <" v "> >. ) )
12	10 11 1	mptfvmpt	|- ( T e. _V -> ( mVH ` T ) = ( v e. V |-> <. ( Y ` v ) , <" v "> >. ) )
13		mpt0	|- ( v e. (/) |-> <. ( Y ` v ) , <" v "> >. ) = (/)
14	13	eqcomi	|- (/) = ( v e. (/) |-> <. ( Y ` v ) , <" v "> >. )
15		fvprc	|- ( -. T e. _V -> ( mVH ` T ) = (/) )
16		fvprc	|- ( -. T e. _V -> ( mVR ` T ) = (/) )
17	1 16	syl5eq	|- ( -. T e. _V -> V = (/) )
18	17	mpteq1d	|- ( -. T e. _V -> ( v e. V |-> <. ( Y ` v ) , <" v "> >. ) = ( v e. (/) |-> <. ( Y ` v ) , <" v "> >. ) )
19	14 15 18	3eqtr4a	|- ( -. T e. _V -> ( mVH ` T ) = ( v e. V |-> <. ( Y ` v ) , <" v "> >. ) )
20	12 19	pm2.61i	|- ( mVH ` T ) = ( v e. V |-> <. ( Y ` v ) , <" v "> >. )
21	3 20	eqtri	|- H = ( v e. V |-> <. ( Y ` v ) , <" v "> >. )