Theorem msrfval

Description: Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msrfval.v	$$⊢V=\mathrm{mVars}\left(T\right)$$
	msrfval.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
	msrfval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
Assertion	msrfval	$$⊢R=\left(s\in P⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		msrfval.v	$$⊢V=\mathrm{mVars}\left(T\right)$$
2		msrfval.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
3		msrfval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
4		fveq2	$$⊢t=T\to \mathrm{mPreSt}\left(t\right)=\mathrm{mPreSt}\left(T\right)$$
5	4 2	eqtr4di	$$⊢t=T\to \mathrm{mPreSt}\left(t\right)=P$$
6		fveq2	$$⊢t=T\to \mathrm{mVars}\left(t\right)=\mathrm{mVars}\left(T\right)$$
7	6 1	eqtr4di	$$⊢t=T\to \mathrm{mVars}\left(t\right)=V$$
8	7	imaeq1d	$$⊢t=T\to \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]=V\left[h\cup \left\{a\right\}\right]$$
9	8	unieqd	$$⊢t=T\to \bigcup \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]=\bigcup V\left[h\cup \left\{a\right\}\right]$$
10	9	csbeq1d	$$⊢t=T\to ⦋\bigcup \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right)=⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right)$$
11	10	ineq2d	$$⊢t=T\to 1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right)=1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right)$$
12	11	oteq1d	$$⊢t=T\to ⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩=⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩$$
13	12	csbeq2dv	$$⊢t=T\to ⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩=⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩$$
14	13	csbeq2dv	$$⊢t=T\to ⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩=⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩$$
15	5 14	mpteq12dv	$$⊢t=T\to \left(s\in \mathrm{mPreSt}\left(t\right)⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)=\left(s\in P⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)$$
16		df-msr	$$⊢\mathrm{mStRed}=\left(t\in \mathrm{V}⟼\left(s\in \mathrm{mPreSt}\left(t\right)⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)\right)$$
17	15 16 2	mptfvmpt	$$⊢T\in \mathrm{V}\to \mathrm{mStRed}\left(T\right)=\left(s\in P⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)$$
18		mpt0	$$⊢\left(s\in \varnothing ⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)=\varnothing$$
19	18	eqcomi	$$⊢\varnothing =\left(s\in \varnothing ⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)$$
20		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mStRed}\left(T\right)=\varnothing$$
21		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mPreSt}\left(T\right)=\varnothing$$
22	2 21	syl5eq	$$⊢\neg T\in \mathrm{V}\to P=\varnothing$$
23	22	mpteq1d	$$⊢\neg T\in \mathrm{V}\to \left(s\in P⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)=\left(s\in \varnothing ⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)$$
24	19 20 23	3eqtr4a	$$⊢\neg T\in \mathrm{V}\to \mathrm{mStRed}\left(T\right)=\left(s\in P⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)$$
25	17 24	pm2.61i	$$⊢\mathrm{mStRed}\left(T\right)=\left(s\in P⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)$$
26	3 25	eqtri	$$⊢R=\left(s\in P⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup V\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)$$