Metamath Proof Explorer


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𝑋 ) )