Theorem msubty

Description: The type of a substituted expression is the same as the original type. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	msubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	msubffval.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
	msubffval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
Assertion	msubty	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( 1st ‘ ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) ) = ( 1st ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		msubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		msubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
3		msubffval.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
4		msubffval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
5		eqid	⊢ ( mRSubst ‘ 𝑇 ) = ( mRSubst ‘ 𝑇 )
6	1 2 3 4 5	msubval	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) = ⟨ ( 1st ‘ 𝑋 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) ⟩ )
7		fvex	⊢ ( 1st ‘ 𝑋 ) ∈ V
8		fvex	⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) ∈ V
9	7 8	op1std	⊢ ( ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) = ⟨ ( 1st ‘ 𝑋 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) ⟩ → ( 1st ‘ ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) ) = ( 1st ‘ 𝑋 ) )
10	6 9	syl	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( 1st ‘ ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) ) = ( 1st ‘ 𝑋 ) )