Description: The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mstaval.r | |
|
mstaval.s | |
||
Assertion | msrid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mstaval.r | |
|
2 | mstaval.s | |
|
3 | eqid | |
|
4 | 3 1 | msrf | |
5 | ffn | |
|
6 | fvelrnb | |
|
7 | 4 5 6 | mp2b | |
8 | 3 | mpst123 | |
9 | 8 | fveq2d | |
10 | id | |
|
11 | 8 10 | eqeltrrd | |
12 | eqid | |
|
13 | eqid | |
|
14 | 12 3 1 13 | msrval | |
15 | 11 14 | syl | |
16 | 9 15 | eqtrd | |
17 | 4 | ffvelcdmi | |
18 | 16 17 | eqeltrrd | |
19 | 12 3 1 13 | msrval | |
20 | 18 19 | syl | |
21 | inass | |
|
22 | inidm | |
|
23 | 22 | ineq2i | |
24 | 21 23 | eqtri | |
25 | 24 | a1i | |
26 | 25 | oteq1d | |
27 | 20 26 | eqtrd | |
28 | 16 | fveq2d | |
29 | 27 28 16 | 3eqtr4d | |
30 | fveq2 | |
|
31 | id | |
|
32 | 30 31 | eqeq12d | |
33 | 29 32 | syl5ibcom | |
34 | 33 | rexlimiv | |
35 | 7 34 | sylbi | |
36 | 1 2 | mstaval | |
37 | 35 36 | eleq2s | |