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∈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∈mFS→mType⁡T:V⟶mTC⁡T
7 6 ffvelcdmda ⊢T∈mFS∧v∈V→mType⁡T⁡v∈mTC⁡T
8 elun2 ⊢v∈V→v∈mCN⁡T∪V
9 8 adantl ⊢T∈mFS∧v∈V→v∈mCN⁡T∪V
10 9 s1cld ⊢T∈mFS∧v∈V→⟨“v”⟩∈WordmCN⁡T∪V
11 eqid ⊢mCN⁡T=mCN⁡T
12 eqid ⊢mREx⁡T=mREx⁡T
13 11 1 12 mrexval ⊢T∈mFS→mREx⁡T=WordmCN⁡T∪V
14 13 adantr ⊢T∈mFS∧v∈V→mREx⁡T=WordmCN⁡T∪V
15 10 14 eleqtrrd ⊢T∈mFS∧v∈V→⟨“v”⟩∈mREx⁡T
16 opelxpi ⊢mType⁡T⁡v∈mTC⁡T∧⟨“v”⟩∈mREx⁡T→mType⁡T⁡v⟨“v”⟩∈mTC⁡T×mREx⁡T
17 7 15 16 syl2anc ⊢T∈mFS∧v∈V→mType⁡T⁡v⟨“v”⟩∈mTC⁡T×mREx⁡T
18 4 2 12 mexval ⊢E=mTC⁡T×mREx⁡T
19 17 18 eleqtrrdi ⊢T∈mFS∧v∈V→mType⁡T⁡v⟨“v”⟩∈E
20 1 5 3 mvhfval ⊢H=v∈V⟼mType⁡T⁡v⟨“v”⟩
21 19 20 fmptd ⊢T∈mFS→H:V⟶E