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 syl5eq ⊢ ¬ 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 ”⟩