| Step |
Hyp |
Ref |
Expression |
| 1 |
|
psdval.s |
|
| 2 |
|
psdval.b |
|
| 3 |
|
psdval.d |
|
| 4 |
|
psdval.x |
|
| 5 |
|
psdval.f |
|
| 6 |
|
fveq1 |
|
| 7 |
6
|
oveq2d |
|
| 8 |
7
|
mpteq2dv |
|
| 9 |
|
reldmpsr |
|
| 10 |
9 1 2
|
elbasov |
|
| 11 |
5 10
|
syl |
|
| 12 |
11
|
simpld |
|
| 13 |
11
|
simprd |
|
| 14 |
1 2 3 12 13 4
|
psdfval |
|
| 15 |
|
ovex |
|
| 16 |
3 15
|
rabex2 |
|
| 17 |
16
|
mptex |
|
| 18 |
17
|
a1i |
|
| 19 |
8 14 5 18
|
fvmptd4 |
|