Metamath Proof Explorer

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∈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∈mVR⁡t⟼mType⁡t⁡v⟨“v”⟩=v∈V⟼Y⁡v⟨“v”⟩
11 df-mvh ⊢mVH=t∈V⟼v∈mVR⁡t⟼mType⁡t⁡v⟨“v”⟩
12 10 11 1 mptfvmpt ⊢T∈V→mVH⁡T=v∈V⟼Y⁡v⟨“v”⟩
13 mpt0 ⊢v∈∅⟼Y⁡v⟨“v”⟩=∅
14 13 eqcomi ⊢∅=v∈∅⟼Y⁡v⟨“v”⟩
15 fvprc ⊢¬T∈V→mVH⁡T=∅
16 fvprc ⊢¬T∈V→mVR⁡T=∅
17 1 16 eqtrid ⊢¬T∈V→V=∅
18 17 mpteq1d ⊢¬T∈V→v∈V⟼Y⁡v⟨“v”⟩=v∈∅⟼Y⁡v⟨“v”⟩
19 14 15 18 3eqtr4a ⊢¬T∈V→mVH⁡T=v∈V⟼Y⁡v⟨“v”⟩
20 12 19 pm2.61i ⊢mVH⁡T=v∈V⟼Y⁡v⟨“v”⟩
21 3 20 eqtri ⊢H=v∈V⟼Y⁡v⟨“v”⟩