Theorem mvhfval 31404

Description: Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016.)

Hypotheses

Ref	Expression
mvhfval.v	⊢ 𝑉 = (mVR‘𝑇)
mvhfval.y	⊢ 𝑌 = (mType‘𝑇)
mvhfval.h	⊢ 𝐻 = (mVH‘𝑇)

Assertion

Ref	Expression
mvhfval	⊢ 𝐻 = (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩)

Distinct variable groups:   𝑣,𝑇   𝑣,𝑉   𝑣,𝑌

Allowed substitution hint:   𝐻(𝑣)

Proof of Theorem mvhfval

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mvhfval.h	. 2 ⊢ 𝐻 = (mVH‘𝑇)
2		fveq2 6178	. . . . . 6 ⊢ (𝑡 = 𝑇 → (mVR‘𝑡) = (mVR‘𝑇))
3		mvhfval.v	. . . . . 6 ⊢ 𝑉 = (mVR‘𝑇)
4	2, 3	syl6eqr 2672	. . . . 5 ⊢ (𝑡 = 𝑇 → (mVR‘𝑡) = 𝑉)
5		fveq2 6178	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (mType‘𝑡) = (mType‘𝑇))
6		mvhfval.y	. . . . . . . 8 ⊢ 𝑌 = (mType‘𝑇)
7	5, 6	syl6eqr 2672	. . . . . . 7 ⊢ (𝑡 = 𝑇 → (mType‘𝑡) = 𝑌)
8	7	fveq1d 6180	. . . . . 6 ⊢ (𝑡 = 𝑇 → ((mType‘𝑡)‘𝑣) = (𝑌‘𝑣))
9	8	opeq1d 4399	. . . . 5 ⊢ (𝑡 = 𝑇 → ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩ = ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩)
10	4, 9	mpteq12dv 4724	. . . 4 ⊢ (𝑡 = 𝑇 → (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩) = (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩))
11		df-mvh 31363	. . . 4 ⊢ mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ ⟨((mType‘𝑡)‘𝑣), ⟨“𝑣”⟩⟩))
12		fvex 6188	. . . . . 6 ⊢ (mVR‘𝑇) ∈ V
13	3, 12	eqeltri 2695	. . . . 5 ⊢ 𝑉 ∈ V
14	13	mptex 6471	. . . 4 ⊢ (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩) ∈ V
15	10, 11, 14	fvmpt 6269	. . 3 ⊢ (𝑇 ∈ V → (mVH‘𝑇) = (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩))
16		mpt0 6008	. . . . 5 ⊢ (𝑣 ∈ ∅ ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩) = ∅
17	16	eqcomi 2629	. . . 4 ⊢ ∅ = (𝑣 ∈ ∅ ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩)
18		fvprc 6172	. . . 4 ⊢ (¬ 𝑇 ∈ V → (mVH‘𝑇) = ∅)
19		fvprc 6172	. . . . . 6 ⊢ (¬ 𝑇 ∈ V → (mVR‘𝑇) = ∅)
20	3, 19	syl5eq 2666	. . . . 5 ⊢ (¬ 𝑇 ∈ V → 𝑉 = ∅)
21	20	mpteq1d 4729	. . . 4 ⊢ (¬ 𝑇 ∈ V → (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩) = (𝑣 ∈ ∅ ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩))
22	17, 18, 21	3eqtr4a 2680	. . 3 ⊢ (¬ 𝑇 ∈ V → (mVH‘𝑇) = (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩))
23	15, 22	pm2.61i 176	. 2 ⊢ (mVH‘𝑇) = (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩)
24	1, 23	eqtri 2642	1 ⊢ 𝐻 = (𝑣 ∈ 𝑉 ↦ ⟨(𝑌‘𝑣), ⟨“𝑣”⟩⟩)

Syntax hints:  ¬ wn 3   = wceq 1481   ∈ wcel 1988  Vcvv 3195  ∅c0 3907  ⟨cop 4174   ↦ cmpt 4720  ‘cfv 5876  ⟨“cs1 13277  mVRcmvar 31332  mTypecmty 31333  mVHcmvh 31343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-mvh 31363

This theorem is referenced by:  mvhval  31405  mvhf  31429