Metamath Proof Explorer

Theorem msrf

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

Ref Expression
Hypotheses mpstssv.p 
|- P = ( mPreSt ` T )
msrf.r 
|- R = ( mStRed ` T )
Assertion msrf 
|- R : P --> P

Proof

Step Hyp Ref Expression
1 mpstssv.p 
 |-  P = ( mPreSt ` T )
2 msrf.r 
 |-  R = ( mStRed ` T )
3 otex 
 |-  <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` T ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. e. _V
4 3 csbex 
 |-  [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` T ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. e. _V
5 4 csbex 
 |-  [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` T ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. e. _V
6 eqid 
 |-  ( mVars ` T ) = ( mVars ` T )
7 6 1 2 msrfval 
 |-  R = ( s e. P |-> [_ ( 2nd ` ( 1st ` s ) ) / h ]_ [_ ( 2nd ` s ) / a ]_ <. ( ( 1st ` ( 1st ` s ) ) i^i [_ U. ( ( mVars ` T ) " ( h u. { a } ) ) / z ]_ ( z X. z ) ) , h , a >. )
8 5 7 fnmpti 
 |-  R Fn P
9 1 mpst123 
 |-  ( s e. P -> s = <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. )
10 9 fveq2d 
 |-  ( s e. P -> ( R ` s ) = ( R ` <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. ) )
11 id 
 |-  ( s e. P -> s e. P )
12 9 11 eqeltrrd 
 |-  ( s e. P -> <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. e. P )
13 eqid 
 |-  U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) = U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) )
14 6 1 2 13 msrval 
 |-  ( <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. e. P -> ( R ` <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. ) = <. ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. )
15 12 14 syl 
 |-  ( s e. P -> ( R ` <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. ) = <. ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. )
16 10 15 eqtrd 
 |-  ( s e. P -> ( R ` s ) = <. ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. )
17 inss1 
 |-  ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) C_ ( 1st ` ( 1st ` s ) )
18 eqid 
 |-  ( mDV ` T ) = ( mDV ` T )
19 eqid 
 |-  ( mEx ` T ) = ( mEx ` T )
20 18 19 1 elmpst 
 |-  ( <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. e. P <-> ( ( ( 1st ` ( 1st ` s ) ) C_ ( mDV ` T ) /\ `' ( 1st ` ( 1st ` s ) ) = ( 1st ` ( 1st ` s ) ) ) /\ ( ( 2nd ` ( 1st ` s ) ) C_ ( mEx ` T ) /\ ( 2nd ` ( 1st ` s ) ) e. Fin ) /\ ( 2nd ` s ) e. ( mEx ` T ) ) )
21 12 20 sylib 
 |-  ( s e. P -> ( ( ( 1st ` ( 1st ` s ) ) C_ ( mDV ` T ) /\ `' ( 1st ` ( 1st ` s ) ) = ( 1st ` ( 1st ` s ) ) ) /\ ( ( 2nd ` ( 1st ` s ) ) C_ ( mEx ` T ) /\ ( 2nd ` ( 1st ` s ) ) e. Fin ) /\ ( 2nd ` s ) e. ( mEx ` T ) ) )
22 21 simp1d 
 |-  ( s e. P -> ( ( 1st ` ( 1st ` s ) ) C_ ( mDV ` T ) /\ `' ( 1st ` ( 1st ` s ) ) = ( 1st ` ( 1st ` s ) ) ) )
23 22 simpld 
 |-  ( s e. P -> ( 1st ` ( 1st ` s ) ) C_ ( mDV ` T ) )
24 17 23 sstrid 
 |-  ( s e. P -> ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) C_ ( mDV ` T ) )
25 cnvin 
 |-  `' ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) = ( `' ( 1st ` ( 1st ` s ) ) i^i `' ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) )
26 22 simprd 
 |-  ( s e. P -> `' ( 1st ` ( 1st ` s ) ) = ( 1st ` ( 1st ` s ) ) )
27 cnvxp 
 |-  `' ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) = ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) )
28 27 a1i 
 |-  ( s e. P -> `' ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) = ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) )
29 26 28 ineq12d 
 |-  ( s e. P -> ( `' ( 1st ` ( 1st ` s ) ) i^i `' ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) = ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) )
30 25 29 syl5eq 
 |-  ( s e. P -> `' ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) = ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) )
31 24 30 jca 
 |-  ( s e. P -> ( ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) C_ ( mDV ` T ) /\ `' ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) = ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) ) )
32 21 simp2d 
 |-  ( s e. P -> ( ( 2nd ` ( 1st ` s ) ) C_ ( mEx ` T ) /\ ( 2nd ` ( 1st ` s ) ) e. Fin ) )
33 21 simp3d 
 |-  ( s e. P -> ( 2nd ` s ) e. ( mEx ` T ) )
34 18 19 1 elmpst 
 |-  ( <. ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. e. P <-> ( ( ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) C_ ( mDV ` T ) /\ `' ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) = ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) ) /\ ( ( 2nd ` ( 1st ` s ) ) C_ ( mEx ` T ) /\ ( 2nd ` ( 1st ` s ) ) e. Fin ) /\ ( 2nd ` s ) e. ( mEx ` T ) ) )
35 31 32 33 34 syl3anbrc 
 |-  ( s e. P -> <. ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. e. P )
36 16 35 eqeltrd 
 |-  ( s e. P -> ( R ` s ) e. P )
37 36 rgen 
 |-  A. s e. P ( R ` s ) e. P
38 ffnfv 
 |-  ( R : P --> P <-> ( R Fn P /\ A. s e. P ( R ` s ) e. P ) )
39 8 37 38 mpbir2an 
 |-  R : P --> P