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	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mvhfval.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
	mvhfval.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
Assertion	mvhfval	⊢ 𝐻 = ( 𝑣 ∈ 𝑉 ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ )

Proof

Step	Hyp	Ref	Expression
1		mvhfval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mvhfval.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
3		mvhfval.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
4		fveq2	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = ( mVR ‘ 𝑇 ) )
5	4 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = 𝑉 )
6		fveq2	⊢ ( 𝑡 = 𝑇 → ( mType ‘ 𝑡 ) = ( mType ‘ 𝑇 ) )
7	6 2	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mType ‘ 𝑡 ) = 𝑌 )
8	7	fveq1d	⊢ ( 𝑡 = 𝑇 → ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) = ( 𝑌 ‘ 𝑣 ) )
9	8	opeq1d	⊢ ( 𝑡 = 𝑇 → ⟨ ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ = ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ )
10	5 9	mpteq12dv	⊢ ( 𝑡 = 𝑇 → ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ⟨ ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) = ( 𝑣 ∈ 𝑉 ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) )
11		df-mvh	⊢ mVH = ( 𝑡 ∈ V ↦ ( 𝑣 ∈ ( mVR ‘ 𝑡 ) ↦ ⟨ ( ( mType ‘ 𝑡 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) )
12	10 11 1	mptfvmpt	⊢ ( 𝑇 ∈ V → ( mVH ‘ 𝑇 ) = ( 𝑣 ∈ 𝑉 ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) )
13		mpt0	⊢ ( 𝑣 ∈ ∅ ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) = ∅
14	13	eqcomi	⊢ ∅ = ( 𝑣 ∈ ∅ ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ )
15		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mVH ‘ 𝑇 ) = ∅ )
16		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mVR ‘ 𝑇 ) = ∅ )
17	1 16	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝑉 = ∅ )
18	17	mpteq1d	⊢ ( ¬ 𝑇 ∈ V → ( 𝑣 ∈ 𝑉 ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) = ( 𝑣 ∈ ∅ ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) )
19	14 15 18	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → ( mVH ‘ 𝑇 ) = ( 𝑣 ∈ 𝑉 ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ) )
20	12 19	pm2.61i	⊢ ( mVH ‘ 𝑇 ) = ( 𝑣 ∈ 𝑉 ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ )
21	3 20	eqtri	⊢ 𝐻 = ( 𝑣 ∈ 𝑉 ↦ ⟨ ( 𝑌 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ )