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=mStRedT
mstaval.s S=mStatT
Assertion msrid XSRX=X

Proof

Step Hyp Ref Expression
1 mstaval.r R=mStRedT
2 mstaval.s S=mStatT
3 eqid mPreStT=mPreStT
4 3 1 msrf R:mPreStTmPreStT
5 ffn R:mPreStTmPreStTRFnmPreStT
6 fvelrnb RFnmPreStTXranRsmPreStTRs=X
7 4 5 6 mp2b XranRsmPreStTRs=X
8 3 mpst123 smPreStTs=1st1sts2nd1sts2nds
9 8 fveq2d smPreStTRs=R1st1sts2nd1sts2nds
10 id smPreStTsmPreStT
11 8 10 eqeltrrd smPreStT1st1sts2nd1sts2ndsmPreStT
12 eqid mVarsT=mVarsT
13 eqid mVarsT2nd1sts2nds=mVarsT2nd1sts2nds
14 12 3 1 13 msrval 1st1sts2nd1sts2ndsmPreStTR1st1sts2nd1sts2nds=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds
15 11 14 syl smPreStTR1st1sts2nd1sts2nds=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds
16 9 15 eqtrd smPreStTRs=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds
17 4 ffvelcdmi smPreStTRsmPreStT
18 16 17 eqeltrrd smPreStT1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2ndsmPreStT
19 12 3 1 13 msrval 1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2ndsmPreStTR1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2ndsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds
20 18 19 syl smPreStTR1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2ndsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds
21 inass 1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2ndsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2ndsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds
22 inidm mVarsT2nd1sts2nds×mVarsT2nd1sts2ndsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds=mVarsT2nd1sts2nds×mVarsT2nd1sts2nds
23 22 ineq2i 1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2ndsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds
24 21 23 eqtri 1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2ndsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds
25 24 a1i smPreStT1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2ndsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds
26 25 oteq1d smPreStT1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2ndsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds
27 20 26 eqtrd smPreStTR1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds=1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds
28 16 fveq2d smPreStTRRs=R1st1stsmVarsT2nd1sts2nds×mVarsT2nd1sts2nds2nd1sts2nds
29 27 28 16 3eqtr4d smPreStTRRs=Rs
30 fveq2 Rs=XRRs=RX
31 id Rs=XRs=X
32 30 31 eqeq12d Rs=XRRs=RsRX=X
33 29 32 syl5ibcom smPreStTRs=XRX=X
34 33 rexlimiv smPreStTRs=XRX=X
35 7 34 sylbi XranRRX=X
36 1 2 mstaval S=ranR
37 35 36 eleq2s XSRX=X