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	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mvhf.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	mvhf.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
Assertion	mvhf	⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 ⟶ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		mvhf.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mvhf.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
3		mvhf.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
4		eqid	⊢ ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 )
5		eqid	⊢ ( mType ‘ 𝑇 ) = ( mType ‘ 𝑇 )
6	1 4 5	mtyf2	⊢ ( 𝑇 ∈ mFS → ( mType ‘ 𝑇 ) : 𝑉 ⟶ ( mTC ‘ 𝑇 ) )
7	6	ffvelcdmda	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑣 ∈ 𝑉 ) → ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) ∈ ( mTC ‘ 𝑇 ) )
8		elun2	⊢ ( 𝑣 ∈ 𝑉 → 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
9	8	adantl	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
10	9	s1cld	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑣 ∈ 𝑉 ) → ⟨“ 𝑣 ”⟩ ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
11		eqid	⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
12		eqid	⊢ ( mREx ‘ 𝑇 ) = ( mREx ‘ 𝑇 )
13	11 1 12	mrexval	⊢ ( 𝑇 ∈ mFS → ( mREx ‘ 𝑇 ) = Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
14	13	adantr	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑣 ∈ 𝑉 ) → ( mREx ‘ 𝑇 ) = Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
15	10 14	eleqtrrd	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑣 ∈ 𝑉 ) → ⟨“ 𝑣 ”⟩ ∈ ( mREx ‘ 𝑇 ) )
16		opelxpi	⊢ ( ( ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) ∈ ( mTC ‘ 𝑇 ) ∧ ⟨“ 𝑣 ”⟩ ∈ ( mREx ‘ 𝑇 ) ) → ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) )
17	7 15 16	syl2anc	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑣 ∈ 𝑉 ) → ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) )
18	4 2 12	mexval	⊢ 𝐸 = ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) )
19	17 18	eleqtrrdi	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑣 ∈ 𝑉 ) → ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ ∈ 𝐸 )
20	1 5 3	mvhfval	⊢ 𝐻 = ( 𝑣 ∈ 𝑉 ↦ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ )
21	19 20	fmptd	⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 ⟶ 𝐸 )