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	$$⊢V=\mathrm{mVR}\left(T\right)$$
	msubffval.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
	msubffval.s	$$⊢S=\mathrm{mSubst}\left(T\right)$$
	msubffval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
Assertion	msubty	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in E\right)\to 1^{st}\left(S\left(F\right)\left(X\right)\right)=1^{st}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		msubffval.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
2		msubffval.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
3		msubffval.s	$$⊢S=\mathrm{mSubst}\left(T\right)$$
4		msubffval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
5		eqid	$$⊢\mathrm{mRSubst}\left(T\right)=\mathrm{mRSubst}\left(T\right)$$
6	1 2 3 4 5	msubval	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in E\right)\to S\left(F\right)\left(X\right)=⟨1^{st}\left(X\right),\mathrm{mRSubst}\left(T\right)\left(F\right)\left(2^{nd}\left(X\right)\right)⟩$$
7		fvex	$$⊢1^{st}\left(X\right)\in \mathrm{V}$$
8		fvex	$$⊢\mathrm{mRSubst}\left(T\right)\left(F\right)\left(2^{nd}\left(X\right)\right)\in \mathrm{V}$$
9	7 8	op1std	$$⊢S\left(F\right)\left(X\right)=⟨1^{st}\left(X\right),\mathrm{mRSubst}\left(T\right)\left(F\right)\left(2^{nd}\left(X\right)\right)⟩\to 1^{st}\left(S\left(F\right)\left(X\right)\right)=1^{st}\left(X\right)$$
10	6 9	syl	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in E\right)\to 1^{st}\left(S\left(F\right)\left(X\right)\right)=1^{st}\left(X\right)$$