Definition df-msr 31391

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

Assertion

Ref	Expression
df-msr	|- mStRed = ( t e. _V |-> ( s e. (mPreSt ` t ) |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( (mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. ) )

Distinct variable group:   h, a, s, t, z

Detailed syntax breakdown of Definition df-msr

Step	Hyp	Ref	Expression
1		cmsr 31371	. 2 class mStRed
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1482	. . . . 5 class t
6		cmpst 31370	. . . . 5 class mPreSt
7	5, 6	cfv 5888	. . . 4 class (mPreSt ` t )
8		vh	. . . . 5 setvar h
9	4	cv 1482	. . . . . . 7 class s
10		c1st 7166	. . . . . . 7 class 1st
11	9, 10	cfv 5888	. . . . . 6 class ( 1st ` s )
12		c2nd 7167	. . . . . 6 class 2nd
13	11, 12	cfv 5888	. . . . 5 class ( 2nd ` ( 1st ` s ) )
14		va	. . . . . 6 setvar a
15	9, 12	cfv 5888	. . . . . 6 class ( 2nd ` s )
16	11, 10	cfv 5888	. . . . . . . 8 class ( 1st ` ( 1st ` s ) )
17		vz	. . . . . . . . 9 setvar z
18		cmvrs 31366	. . . . . . . . . . . 12 class mVars
19	5, 18	cfv 5888	. . . . . . . . . . 11 class (mVars ` t )
20	8	cv 1482	. . . . . . . . . . . 12 class h
21	14	cv 1482	. . . . . . . . . . . . 13 class a
22	21	csn 4177	. . . . . . . . . . . 12 class { a }
23	20, 22	cun 3572	. . . . . . . . . . 11 class ( h u. { a } )
24	19, 23	cima 5117	. . . . . . . . . 10 class ( (mVars ` t ) " ( h u. { a } ) )
25	24	cuni 4436	. . . . . . . . 9 class U. ( (mVars ` t ) " ( h u. { a } ) )
26	17	cv 1482	. . . . . . . . . 10 class z
27	26, 26	cxp 5112	. . . . . . . . 9 class ( z X. z )
28	17, 25, 27	csb 3533	. . . . . . . 8 class [_ U. ( (mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z )
29	16, 28	cin 3573	. . . . . . 7 class ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( (mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) )
30	29, 20, 21	cotp 4185	. . . . . 6 class <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( (mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >.
31	14, 15, 30	csb 3533	. . . . 5 class [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( (mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >.
32	8, 13, 31	csb 3533	. . . 4 class [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( (mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >.
33	4, 7, 32	cmpt 4729	. . 3 class ( s e. (mPreSt ` t ) |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( (mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )
34	2, 3, 33	cmpt 4729	. 2 class ( t e. _V |-> ( s e. (mPreSt ` t ) |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( (mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. ) )
35	1, 34	wceq 1483	1 wff mStRed = ( t e. _V |-> ( s e. (mPreSt ` t ) |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( (mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. ) )

This definition is referenced by:  msrfval  31434