Metamath Proof Explorer

Theorem msrid

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

Ref Expression
Hypotheses mstaval.r 
|- R = ( mStRed ` T )
mstaval.s 
|- S = ( mStat ` T )
Assertion msrid 
|- ( X e. S -> ( R ` X ) = X )

Proof

Step Hyp Ref Expression
1 mstaval.r 
 |-  R = ( mStRed ` T )
2 mstaval.s 
 |-  S = ( mStat ` T )
3 eqid 
 |-  ( mPreSt ` T ) = ( mPreSt ` T )
4 3 1 msrf 
 |-  R : ( mPreSt ` T ) --> ( mPreSt ` T )
5 ffn 
 |-  ( R : ( mPreSt ` T ) --> ( mPreSt ` T ) -> R Fn ( mPreSt ` T ) )
6 fvelrnb 
 |-  ( R Fn ( mPreSt ` T ) -> ( X e. ran R <-> E. s e. ( mPreSt ` T ) ( R ` s ) = X ) )
7 4 5 6 mp2b 
 |-  ( X e. ran R <-> E. s e. ( mPreSt ` T ) ( R ` s ) = X )
8 3 mpst123 
 |-  ( s e. ( mPreSt ` T ) -> s = <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. )
9 8 fveq2d 
 |-  ( s e. ( mPreSt ` T ) -> ( R ` s ) = ( R ` <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. ) )
10 id 
 |-  ( s e. ( mPreSt ` T ) -> s e. ( mPreSt ` T ) )
11 8 10 eqeltrrd 
 |-  ( s e. ( mPreSt ` T ) -> <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. e. ( mPreSt ` T ) )
12 eqid 
 |-  ( mVars ` T ) = ( mVars ` T )
13 eqid 
 |-  U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) = U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) )
14 12 3 1 13 msrval 
 |-  ( <. ( 1st ` ( 1st ` s ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. e. ( mPreSt ` T ) -> ( 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 11 14 syl 
 |-  ( s e. ( mPreSt ` T ) -> ( 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 9 15 eqtrd 
 |-  ( s e. ( mPreSt ` T ) -> ( 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 4 ffvelrni 
 |-  ( s e. ( mPreSt ` T ) -> ( R ` s ) e. ( mPreSt ` T ) )
18 16 17 eqeltrrd 
 |-  ( s e. ( mPreSt ` 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 ) } ) ) ) ) , ( 2nd ` ( 1st ` s ) ) , ( 2nd ` s ) >. e. ( mPreSt ` T ) )
19 12 3 1 13 msrval 
 |-  ( <. ( ( 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. ( mPreSt ` T ) -> ( R ` <. ( ( 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 ) >. ) = <. ( ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` 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 ) >. )
20 18 19 syl 
 |-  ( s e. ( mPreSt ` T ) -> ( R ` <. ( ( 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 ) >. ) = <. ( ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` 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 ) >. )
21 inass 
 |-  ( ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` 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 ) } ) ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) ) )
22 inidm 
 |-  ( ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) ) i^i ( 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 ) } ) ) )
23 22 ineq2i 
 |-  ( ( 1st ` ( 1st ` s ) ) i^i ( ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` 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 ) } ) ) ) )
24 21 23 eqtri 
 |-  ( ( ( 1st ` ( 1st ` s ) ) i^i ( U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` s ) } ) ) X. U. ( ( mVars ` T ) " ( ( 2nd ` ( 1st ` s ) ) u. { ( 2nd ` 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 ) } ) ) ) )
25 24 a1i 
 |-  ( s e. ( mPreSt ` 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 ) } ) ) ) ) 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 25 oteq1d 
 |-  ( s e. ( mPreSt ` 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 ) } ) ) ) ) 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 ) >. = <. ( ( 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 ) >. )
27 20 26 eqtrd 
 |-  ( s e. ( mPreSt ` T ) -> ( R ` <. ( ( 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 ) >. ) = <. ( ( 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 ) >. )
28 16 fveq2d 
 |-  ( s e. ( mPreSt ` T ) -> ( R ` ( R ` s ) ) = ( R ` <. ( ( 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 ) >. ) )
29 27 28 16 3eqtr4d 
 |-  ( s e. ( mPreSt ` T ) -> ( R ` ( R ` s ) ) = ( R ` s ) )
30 fveq2 
 |-  ( ( R ` s ) = X -> ( R ` ( R ` s ) ) = ( R ` X ) )
31 id 
 |-  ( ( R ` s ) = X -> ( R ` s ) = X )
32 30 31 eqeq12d 
 |-  ( ( R ` s ) = X -> ( ( R ` ( R ` s ) ) = ( R ` s ) <-> ( R ` X ) = X ) )
33 29 32 syl5ibcom 
 |-  ( s e. ( mPreSt ` T ) -> ( ( R ` s ) = X -> ( R ` X ) = X ) )
34 33 rexlimiv 
 |-  ( E. s e. ( mPreSt ` T ) ( R ` s ) = X -> ( R ` X ) = X )
35 7 34 sylbi 
 |-  ( X e. ran R -> ( R ` X ) = X )
36 1 2 mstaval 
 |-  S = ran R
37 35 36 eleq2s 
 |-  ( X e. S -> ( R ` X ) = X )