Metamath Proof Explorer

Theorem msrfval

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

Ref Expression
Hypotheses msrfval.v 
|- V = ( mVars ` T )
msrfval.p 
|- P = ( mPreSt ` T )
msrfval.r 
|- R = ( mStRed ` T )
Assertion msrfval 
|- R = ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )

Proof

Step Hyp Ref Expression
1 msrfval.v 
 |-  V = ( mVars ` T )
2 msrfval.p 
 |-  P = ( mPreSt ` T )
3 msrfval.r 
 |-  R = ( mStRed ` T )
4 fveq2 
 |-  ( t = T -> ( mPreSt ` t ) = ( mPreSt ` T ) )
5 4 2 eqtr4di 
 |-  ( t = T -> ( mPreSt ` t ) = P )
6 fveq2 
 |-  ( t = T -> ( mVars ` t ) = ( mVars ` T ) )
7 6 1 eqtr4di 
 |-  ( t = T -> ( mVars ` t ) = V )
8 7 imaeq1d 
 |-  ( t = T -> ( ( mVars ` t ) " ( h u. { a } ) ) = ( V " ( h u. { a } ) ) )
9 8 unieqd 
 |-  ( t = T -> U. ( ( mVars ` t ) " ( h u. { a } ) ) = U. ( V " ( h u. { a } ) ) )
10 9 csbeq1d 
 |-  ( t = T -> [_ U. ( ( mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) = [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) )
11 10 ineq2d 
 |-  ( t = T -> ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) = ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) )
12 11 oteq1d 
 |-  ( t = T -> <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. = <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )
13 12 csbeq2dv 
 |-  ( t = T -> [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` t ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. = [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )
14 13 csbeq2dv 
 |-  ( t = 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 >. = [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )
15 5 14 mpteq12dv 
 |-  ( t = T -> ( 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 >. ) = ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. ) )
16 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 >. ) )
17 15 16 2 mptfvmpt 
 |-  ( T e. _V -> ( mStRed ` T ) = ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. ) )
18 mpt0 
 |-  ( s e. (/) |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. ) = (/)
19 18 eqcomi 
 |-  (/) = ( s e. (/) |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )
20 fvprc 
 |-  ( -. T e. _V -> ( mStRed ` T ) = (/) )
21 fvprc 
 |-  ( -. T e. _V -> ( mPreSt ` T ) = (/) )
22 2 21 syl5eq 
 |-  ( -. T e. _V -> P = (/) )
23 22 mpteq1d 
 |-  ( -. T e. _V -> ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. ) = ( s e. (/) |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. ) )
24 19 20 23 3eqtr4a 
 |-  ( -. T e. _V -> ( mStRed ` T ) = ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. ) )
25 17 24 pm2.61i 
 |-  ( mStRed ` T ) = ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )
26 3 25 eqtri 
 |-  R = ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( V " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )