Metamath Proof Explorer

Definition df-msr

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmsr 
 |-  mStRed
1 vt 
 |-  t
2 cvv 
 |-  _V
3 vs 
 |-  s
4 cmpst 
 |-  mPreSt
5 1 cv 
 |-  t
6 5 4 cfv 
 |-  ( mPreSt ` t )
7 c2nd 
 |-  2nd
8 c1st 
 |-  1st
9 3 cv 
 |-  s
10 9 8 cfv 
 |-  ( 1st ` s )
11 10 7 cfv 
 |-  ( 2nd ` ( 1st ` s ) )
12 vh 
 |-  h
13 9 7 cfv 
 |-  ( 2nd ` s )
14 va 
 |-  a
15 10 8 cfv 
 |-  ( 1st ` ( 1st ` s ) )
16 cmvrs 
 |-  mVars
17 5 16 cfv 
 |-  ( mVars ` t )
18 12 cv 
 |-  h
19 14 cv 
 |-  a
20 19 csn 
 |-  { a }
21 18 20 cun 
 |-  ( h u. { a } )
22 17 21 cima 
 |-  ( ( mVars ` t ) " ( h u. { a } ) )
23 22 cuni 
 |-  U. ( ( mVars ` t ) " ( h u. { a } ) )
24 vz 
 |-  z
25 24 cv 
 |-  z
26 25 25 cxp 
 |-  ( z X. z )
27 24 23 26 csb 
 |-  [_ U. ( ( mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z )
28 15 27 cin 
 |-  ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) )
29 28 18 19 cotp 
 |-  <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >.
30 14 13 29 csb 
 |-  [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >.
31 12 11 30 csb 
 |-  [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >.
32 3 6 31 cmpt 
 |-  ( 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 >. )
33 1 2 32 cmpt 
 |-  ( 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 >. ) )
34 0 33 wceq 
 |-  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 >. ) )