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 ffvelrnda ⊢ 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 ”⟩ ∈ Word mCN ⁡ T ∪ V
11 eqid ⊢ mCN ⁡ T = mCN ⁡ T
12 eqid ⊢ mREx ⁡ T = mREx ⁡ T
13 11 1 12 mrexval ⊢ T ∈ mFS → mREx ⁡ T = Word mCN ⁡ T ∪ V
14 13 adantr ⊢ T ∈ mFS ∧ v ∈ V → mREx ⁡ T = Word mCN ⁡ 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