Definition df-msr

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

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmsr	$$class\mathrm{mStRed}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		cmpst	$$class\mathrm{mPreSt}$$
5	1	cv	$$setvart$$
6	5 4	cfv	$$class\mathrm{mPreSt}\left(t\right)$$
7		c2nd	$$class{2}^{nd}$$
8		c1st	$$class{1}^{st}$$
9	3	cv	$$setvars$$
10	9 8	cfv	$$class{1}^{st}\left(s\right)$$
11	10 7	cfv	$$class{2}^{nd}\left(1^{st}\left(s\right)\right)$$
12		vh	$$setvarh$$
13	9 7	cfv	$$class{2}^{nd}\left(s\right)$$
14		va	$$setvara$$
15	10 8	cfv	$$class{1}^{st}\left(1^{st}\left(s\right)\right)$$
16		cmvrs	$$class\mathrm{mVars}$$
17	5 16	cfv	$$class\mathrm{mVars}\left(t\right)$$
18	12	cv	$$setvarh$$
19	14	cv	$$setvara$$
20	19	csn	$$class\left\{a\right\}$$
21	18 20	cun	$$class\left(h\cup \left\{a\right\}\right)$$
22	17 21	cima	$$class\mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]$$
23	22	cuni	$$class\bigcup \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]$$
24		vz	$$setvarz$$
25	24	cv	$$setvarz$$
26	25 25	cxp	$$class\left(z\times z\right)$$
27	24 23 26	csb	$$class⦋\bigcup \mathrm{mVars}\left(t\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right)$$
28	15 27	cin	$$class\left(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)\right)$$
29	28 18 19	cotp	$$class⟨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⟩$$
30	14 13 29	csb	$$class⦋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⟩$$
31	12 11 30	csb	$$class⦋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⟩$$
32	3 6 31	cmpt	$$class\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)$$
33	1 2 32	cmpt	$$class\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)$$
34	0 33	wceq	$$wff\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)$$